fof(t140_complex1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => r1_xreal_0(k3_complex1(A),k17_complex1(A)) ) ),
    inference(mizar_proof,[status(thm)],[t72_square_1,t9_xreal_1,t72_square_1,t94_square_1,l182_complex1,l187_complex1,t2_xreal_1]),
    [file(complex1,t140_complex1),interesting(1.00)]).

fof(t141_complex1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => r1_xreal_0(k4_complex1(A),k17_complex1(A)) ) ),
    inference(mizar_proof,[status(thm)],[t72_square_1,t9_xreal_1,t72_square_1,t94_square_1,l182_complex1,l187_complex1,t2_xreal_1]),
    [file(complex1,t141_complex1),interesting(1.00)]).

fof(t150_complex1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => r1_xreal_0(k17_complex1(k5_real_1(k17_complex1(A),k17_complex1(B))),k17_complex1(k6_xcmplx_0(A,B))) ) ) ),
    inference(mizar_proof,[status(thm)],[t145_complex1,t146_complex1,t26_xreal_1,t145_complex1,l198_complex1]),
    [file(complex1,t150_complex1),interesting(0.96)]).

fof(t139_complex1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => k17_complex1(k15_complex1(A)) = k17_complex1(A) ) ),
    inference(mizar_proof,[status(thm)],[t112_complex1,t112_complex1]),
    [file(complex1,t139_complex1),interesting(0.93)]).

fof(t119_complex1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k2_numbers)
     => k15_complex1(k10_complex1(A)) = k10_complex1(k15_complex1(A)) ) ),
    inference(mizar_proof,[status(thm)],[t112_complex1,t34_complex1,t112_complex1,t34_complex1,d5_complex1,t112_complex1,t34_complex1,t112_complex1,t34_complex1]),
    [file(complex1,t119_complex1),interesting(0.92)]).

fof(l180_complex1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => k17_complex1(k4_xcmplx_0(A)) = k17_complex1(A) ) ),
    inference(mizar_proof,[status(thm)],[t34_complex1,t34_complex1]),
    [file(complex1,l180_complex1),interesting(0.92)]).

fof(l182_complex1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => k8_square_1(k5_square_1(A)) = k17_complex1(A) ) ),
    inference(mizar_proof,[status(thm)],[t129_complex1,t89_square_1,l181_complex1,t90_square_1]),
    [file(complex1,l182_complex1),interesting(0.92)]).

fof(t152_complex1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => k17_complex1(k5_xcmplx_0(A)) = k2_real_1(k17_complex1(A)) ) ),
    inference(mizar_proof,[status(thm)],[t13_complex1,l5_complex1,t64_complex1,t64_complex1,t69_square_1,t69_square_1,t63_xcmplx_1,t92_xcmplx_1,t83_square_1,t99_square_1,t217_xcmplx_1,l170_complex1,t12_complex1,l170_complex1,t12_complex1]),
    [file(complex1,t152_complex1),interesting(0.91)]).

fof(t122_complex1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k2_numbers)
     => k15_complex1(k12_complex1(A)) = k12_complex1(k15_complex1(A)) ) ),
    inference(mizar_proof,[status(thm)],[t112_complex1,t112_complex1,t64_complex1,t64_complex1,d5_complex1,t112_complex1,t64_complex1,t188_xcmplx_1,t64_complex1]),
    [file(complex1,t122_complex1),interesting(0.90)]).

fof(t143_complex1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => r1_xreal_0(k17_complex1(k6_xcmplx_0(A,B)),k3_real_1(k17_complex1(A),k17_complex1(B))) ) ) ),
    inference(mizar_proof,[status(thm)],[t142_complex1,l180_complex1]),
    [file(complex1,t143_complex1),interesting(0.90)]).

fof(t120_complex1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k2_numbers)
     => ! [B] : 
          ( m1_subset_1(B,k2_numbers)
         => k15_complex1(k11_complex1(A,B)) = k11_complex1(k15_complex1(A),k15_complex1(B)) ) ) ),
    inference(mizar_proof,[status(thm)],[t118_complex1,t119_complex1]),
    [file(complex1,t120_complex1),interesting(0.89)]).

fof(t145_complex1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => r1_xreal_0(k5_real_1(k17_complex1(A),k17_complex1(B)),k17_complex1(k6_xcmplx_0(A,B))) ) ) ),
    inference(mizar_proof,[status(thm)],[t142_complex1,t22_xreal_1]),
    [file(complex1,t145_complex1),interesting(0.89)]).

fof(t142_complex1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => r1_xreal_0(k17_complex1(k2_xcmplx_0(A,B)),k3_real_1(k17_complex1(A),k17_complex1(B))) ) ) ),
    inference(mizar_proof,[status(thm)],[l5_complex1,d4_square_1,t19_complex1,t19_complex1,t72_square_1,t21_xreal_1,t72_square_1,l187_complex1,t94_square_1,l182_complex1,t97_square_1,t2_xreal_1,t66_xreal_1,t9_xreal_1,t9_xreal_1,l5_complex1,d4_square_1,t9_xreal_1,t94_square_1,t89_square_1]),
    [file(complex1,t142_complex1),interesting(0.88)]).

fof(l198_complex1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ( ( r1_xreal_0(k4_xcmplx_0(B),A)
              & r1_xreal_0(A,B) )
          <=> r1_xreal_0(k17_complex1(A),B) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t26_xreal_1,l181_complex1,t129_complex1,t132_complex1,t26_xreal_1,t129_complex1,l181_complex1,t26_xreal_1,t132_complex1,t26_xreal_1]),
    [file(complex1,l198_complex1),interesting(0.88)]).

fof(t116_complex1,theorem,(
    k15_complex1(k7_complex1) = k10_complex1(k7_complex1) ),
    inference(mizar_proof,[status(thm)],[l69_complex1,l155_complex1,t9_complex1]),
    [file(complex1,t116_complex1),interesting(0.87)]).

fof(t118_complex1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => k15_complex1(k2_xcmplx_0(A,B)) = k8_complex1(k15_complex1(A),k15_complex1(B)) ) ) ),
    inference(mizar_proof,[status(thm)],[t112_complex1,t19_complex1,t112_complex1,t112_complex1,t19_complex1,d5_complex1,t112_complex1,t19_complex1,t112_complex1,t112_complex1,t19_complex1]),
    [file(complex1,t118_complex1),interesting(0.87)]).

fof(l187_complex1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ( r1_xreal_0(k1_real_1(k17_complex1(A)),A)
        & r1_xreal_0(A,k17_complex1(A)) ) ) ),
    inference(mizar_proof,[status(thm)],[l181_complex1,t60_xreal_1,t26_xreal_1,t129_complex1]),
    [file(complex1,l187_complex1),interesting(0.87)]).

fof(t158_complex1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => k8_square_1(k5_square_1(A)) = k17_complex1(A) ) ),
    inference(mizar_proof,[status(thm)],[l182_complex1]),
    [file(complex1,t158_complex1),interesting(0.87)]).

fof(t157_complex1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ( k17_complex1(A) = A
        | k17_complex1(A) = k4_xcmplx_0(A) ) ) ),
    inference(mizar_proof,[status(thm)],[t129_complex1,l181_complex1]),
    [file(complex1,t157_complex1),interesting(0.87)]).

fof(l46_complex1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k1_numbers)
     => k4_complex1(k3_xcmplx_0(A,k7_complex1)) = A ) ),
    inference(mizar_proof,[status(thm)],[l43_complex1,d2_complex1,t17_complex1]),
    [file(complex1,l46_complex1),interesting(0.86)]).

fof(l181_complex1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ( r1_xreal_0(A,0)
       => k17_complex1(A) = k4_xcmplx_0(A) ) ) ),
    inference(mizar_proof,[status(thm)],[t26_xreal_1,t129_complex1,l180_complex1]),
    [file(complex1,l181_complex1),interesting(0.86)]).

fof(t138_complex1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => k17_complex1(k4_xcmplx_0(A)) = k17_complex1(A) ) ),
    inference(mizar_proof,[status(thm)],[l180_complex1]),
    [file(complex1,t138_complex1),interesting(0.86)]).

fof(t161_complex1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => k7_square_1(k17_complex1(A)) = k5_square_1(A) ) ),
    inference(mizar_proof,[status(thm)],[t157_complex1]),
    [file(complex1,t161_complex1),interesting(0.86)]).

fof(t26_complex1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k1_numbers)
     => k4_complex1(k3_xcmplx_0(A,k7_complex1)) = A ) ),
    inference(mizar_proof,[status(thm)],[t24_complex1,d2_complex1,t17_complex1]),
    [file(complex1,t26_complex1),interesting(0.86)]).

fof(l35_complex1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k1_numbers)
     => k3_arytm_0(A) = k1_real_1(A) ) ),
    inference(mizar_proof,[status(thm)],[d4_arytm_0,l34_complex1]),
    [file(complex1,l35_complex1),interesting(0.85)]).

fof(t144_complex1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => r1_xreal_0(k5_real_1(k17_complex1(A),k17_complex1(B)),k17_complex1(k2_xcmplx_0(A,B))) ) ) ),
    inference(mizar_proof,[status(thm)],[t143_complex1,t22_xreal_1]),
    [file(complex1,t144_complex1),interesting(0.85)]).

fof(t146_complex1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => k17_complex1(k6_xcmplx_0(A,B)) = k17_complex1(k6_xcmplx_0(B,A)) ) ) ),
    inference(mizar_proof,[status(thm)],[l180_complex1]),
    [file(complex1,t146_complex1),interesting(0.85)]).

fof(l13_complex1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => k5_arytm_0(k3_complex1(A),k4_complex1(A)) = A ) ),
    inference(mizar_proof,[status(thm)],[d2_xcmplx_0,d3_complex1,d7_arytm_0,d2_complex1,d3_complex1,d2_complex1,t5_complex1,t66_funct_4,t66_funct_4,l1_complex1,l2_complex1,d2_numbers,d2_xboole_0,d4_xboole_0,l1_complex1,l2_complex1,t11_funct_2,t66_funct_4,l1_complex1,d7_arytm_0]),
    [file(complex1,l13_complex1),interesting(0.84)]).

fof(t123_complex1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k2_numbers)
     => ! [B] : 
          ( m1_subset_1(B,k2_numbers)
         => k15_complex1(k13_complex1(A,B)) = k13_complex1(k15_complex1(A),k15_complex1(B)) ) ) ),
    inference(mizar_proof,[status(thm)],[d9_xcmplx_0,t121_complex1,t122_complex1,d9_xcmplx_0]),
    [file(complex1,t123_complex1),interesting(0.84)]).

fof(t131_complex1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ( k17_complex1(A) = 0
       => A = 0 ) ) ),
    inference(mizar_proof,[status(thm)],[l5_complex1,t92_square_1,t13_complex1]),
    [file(complex1,t131_complex1),interesting(0.83)]).

fof(t114_complex1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ( k15_complex1(A) = 0
       => A = 0 ) ) ),
    inference(mizar_proof,[status(thm)],[t28_complex1,t12_complex1,l23_complex1,l12_complex1,d5_complex1]),
    [file(complex1,t114_complex1),interesting(0.81)]).

fof(t151_complex1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => k17_complex1(k3_xcmplx_0(A,B)) = k4_real_1(k17_complex1(A),k17_complex1(B)) ) ) ),
    inference(mizar_proof,[status(thm)],[l5_complex1,t24_complex1,t24_complex1,t97_square_1]),
    [file(complex1,t151_complex1),interesting(0.81)]).

fof(t162_complex1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ( r1_xreal_0(k1_real_1(k17_complex1(A)),A)
        & r1_xreal_0(A,k17_complex1(A)) ) ) ),
    inference(mizar_proof,[status(thm)],[l187_complex1]),
    [file(complex1,t162_complex1),interesting(0.81)]).

fof(l45_complex1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k1_numbers)
     => k3_complex1(k3_xcmplx_0(A,k7_complex1)) = 0 ) ),
    inference(mizar_proof,[status(thm)],[l43_complex1,d3_complex1,t17_complex1]),
    [file(complex1,l45_complex1),interesting(0.80)]).

fof(t121_complex1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k2_numbers)
     => ! [B] : 
          ( m1_subset_1(B,k2_numbers)
         => k15_complex1(k9_complex1(A,B)) = k9_complex1(k15_complex1(A),k15_complex1(B)) ) ) ),
    inference(mizar_proof,[status(thm)],[t112_complex1,t112_complex1,t112_complex1,t24_complex1,t24_complex1,d5_complex1,t112_complex1,t24_complex1,t24_complex1]),
    [file(complex1,t121_complex1),interesting(0.80)]).

fof(t155_complex1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => k17_complex1(k3_xcmplx_0(A,A)) = k17_complex1(k3_xcmplx_0(A,k15_complex1(A))) ) ),
    inference(mizar_proof,[status(thm)],[t151_complex1,t139_complex1,t151_complex1]),
    [file(complex1,t155_complex1),interesting(0.80)]).

fof(t25_complex1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k1_numbers)
     => k3_complex1(k3_xcmplx_0(A,k7_complex1)) = 0 ) ),
    inference(mizar_proof,[status(thm)],[t24_complex1,d3_complex1,t17_complex1]),
    [file(complex1,t25_complex1),interesting(0.80)]).

fof(t147_complex1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ( k17_complex1(k6_xcmplx_0(A,B)) = 0
          <=> A = B ) ) ) ),
    inference(mizar_proof,[status(thm)],[t131_complex1,t130_complex1]),
    [file(complex1,t147_complex1),interesting(0.79)]).

fof(t156_complex1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ( r1_xreal_0(A,0)
       => k17_complex1(A) = k4_xcmplx_0(A) ) ) ),
    inference(mizar_proof,[status(thm)],[l181_complex1]),
    [file(complex1,t156_complex1),interesting(0.79)]).

fof(t153_complex1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => k6_real_1(k17_complex1(A),k17_complex1(B)) = k17_complex1(k7_xcmplx_0(A,B)) ) ) ),
    inference(mizar_proof,[status(thm)],[d9_xcmplx_0,t152_complex1,t151_complex1,d9_xcmplx_0]),
    [file(complex1,t153_complex1),interesting(0.78)]).

fof(t9_complex1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ( ( k3_complex1(A) = k3_complex1(B)
              & k4_complex1(A) = k4_complex1(B) )
           => A = B ) ) ) ),
    inference(mizar_proof,[status(thm)],[l13_complex1,l13_complex1]),
    [file(complex1,t9_complex1),interesting(0.75)]).

fof(t124_complex1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k2_numbers)
     => ( k4_complex1(A) = 0
       => k15_complex1(A) = A ) ) ),
    inference(mizar_proof,[status(thm)],[t112_complex1,t9_complex1]),
    [file(complex1,t124_complex1),interesting(0.75)]).

fof(t29_complex1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => k2_xcmplx_0(k3_complex1(A),k3_xcmplx_0(k4_complex1(A),k7_complex1)) = A ) ),
    inference(mizar_proof,[status(thm)],[l13_complex1,l47_complex1]),
    [file(complex1,t29_complex1),interesting(0.74)]).

fof(l47_complex1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k1_numbers)
     => ! [B] : 
          ( m1_subset_1(B,k1_numbers)
         => k5_arytm_0(A,B) = k2_xcmplx_0(A,k3_xcmplx_0(B,k7_complex1)) ) ) ),
    inference(mizar_proof,[status(thm)],[l44_complex1,l45_complex1,d2_complex1,l44_complex1,d3_complex1,l46_complex1,l13_complex1]),
    [file(complex1,l47_complex1),interesting(0.73)]).

fof(t112_complex1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ( k3_complex1(k15_complex1(A)) = k3_complex1(A)
        & k4_complex1(k15_complex1(A)) = k1_real_1(k4_complex1(A)) ) ) ),
    inference(mizar_proof,[status(thm)],[t28_complex1]),
    [file(complex1,t112_complex1),interesting(0.73)]).

fof(t149_complex1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => r1_xreal_0(k17_complex1(k6_xcmplx_0(B,C)),k3_real_1(k17_complex1(k6_xcmplx_0(B,A)),k17_complex1(k6_xcmplx_0(A,C)))) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t142_complex1]),
    [file(complex1,t149_complex1),interesting(0.73)]).

fof(t136_complex1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ( k4_complex1(A) = 0
       => k17_complex1(A) = k17_complex1(k3_complex1(A)) ) ) ),
    inference(mizar_proof,[status(thm)],[l182_complex1]),
    [file(complex1,t136_complex1),interesting(0.71)]).

fof(t137_complex1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ( k3_complex1(A) = 0
       => k17_complex1(A) = k17_complex1(k4_complex1(A)) ) ) ),
    inference(mizar_proof,[status(thm)],[l182_complex1]),
    [file(complex1,t137_complex1),interesting(0.71)]).

fof(t34_complex1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ( k3_complex1(k4_xcmplx_0(A)) = k1_real_1(k3_complex1(A))
        & k4_complex1(k4_xcmplx_0(A)) = k1_real_1(k4_complex1(A)) ) ) ),
    inference(mizar_proof,[status(thm)],[d2_xcmplx_0,d11_complex1,t28_complex1]),
    [file(complex1,t34_complex1),interesting(0.70)]).

fof(t13_complex1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ( A = 0
      <=> k3_real_1(k7_square_1(k3_complex1(A)),k7_square_1(k4_complex1(A))) = 0 ) ) ),
    inference(mizar_proof,[status(thm)],[t12_complex1,t2_complex1,t9_complex1,t12_complex1]),
    [file(complex1,t13_complex1),interesting(0.65)]).

fof(l69_complex1,theorem,
    ( k3_complex1(k10_complex1(k7_complex1)) = 0
    & k4_complex1(k10_complex1(k7_complex1)) = k1_real_1(1) ),
    inference(mizar_proof,[status(thm)],[l68_complex1,t28_complex1]),
    [file(complex1,l69_complex1),interesting(0.64)]).

fof(l155_complex1,theorem,
    ( k3_complex1(k15_complex1(k7_complex1)) = 0
    & k4_complex1(k15_complex1(k7_complex1)) = k1_real_1(1) ),
    inference(mizar_proof,[status(thm)],[t17_complex1,t112_complex1]),
    [file(complex1,l155_complex1),interesting(0.64)]).

fof(t154_complex1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => k17_complex1(k3_xcmplx_0(A,A)) = k3_real_1(k7_square_1(k3_complex1(A)),k7_square_1(k4_complex1(A))) ) ),
    inference(mizar_proof,[status(thm)],[l5_complex1,t151_complex1,t97_square_1,t89_square_1]),
    [file(complex1,t154_complex1),interesting(0.64)]).

fof(t27_complex1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k1_numbers)
     => ! [B] : 
          ( m1_subset_1(B,k1_numbers)
         => k5_arytm_0(A,B) = k2_xcmplx_0(A,k3_xcmplx_0(B,k7_complex1)) ) ) ),
    inference(mizar_proof,[status(thm)],[t19_complex1,t25_complex1,d2_complex1,t19_complex1,d3_complex1,t26_complex1,l13_complex1]),
    [file(complex1,t27_complex1),interesting(0.64)]).

fof(l44_complex1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ( k3_complex1(k2_xcmplx_0(A,B)) = k3_real_1(k3_complex1(A),k3_complex1(B))
            & k4_complex1(k2_xcmplx_0(A,B)) = k3_real_1(k4_complex1(A),k4_complex1(B)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d2_xcmplx_0,l41_complex1,l12_complex1]),
    [file(complex1,l44_complex1),interesting(0.63)]).

fof(t19_complex1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ( k3_complex1(k2_xcmplx_0(A,B)) = k3_real_1(k3_complex1(A),k3_complex1(B))
            & k4_complex1(k2_xcmplx_0(A,B)) = k3_real_1(k4_complex1(A),k4_complex1(B)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d2_xcmplx_0,l41_complex1,l12_complex1]),
    [file(complex1,t19_complex1),interesting(0.63)]).

fof(l37_complex1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k2_numbers)
     => ! [B] : 
          ( m1_subset_1(B,k2_numbers)
         => ! [C] : 
              ( m1_subset_1(C,k2_numbers)
             => ( C = k2_xcmplx_0(A,B)
               => k3_complex1(C) = k3_real_1(k3_complex1(A),k3_complex1(B)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d4_xcmplx_0,l12_complex1,l12_complex1,l34_complex1]),
    [file(complex1,l37_complex1),interesting(0.62)]).

fof(l38_complex1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k2_numbers)
     => ! [B] : 
          ( m1_subset_1(B,k2_numbers)
         => ! [C] : 
              ( m1_subset_1(C,k2_numbers)
             => ( C = k2_xcmplx_0(A,B)
               => k4_complex1(C) = k3_real_1(k4_complex1(A),k4_complex1(B)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d4_xcmplx_0,l12_complex1,l12_complex1,l34_complex1]),
    [file(complex1,l38_complex1),interesting(0.62)]).

fof(t133_complex1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ( ~ ( A != 0
            & r1_xreal_0(k17_complex1(A),0) )
        & ~ ( ~ r1_xreal_0(k17_complex1(A),0)
            & A = 0 ) ) ) ),
    inference(mizar_proof,[status(thm)],[t131_complex1,t132_complex1,l170_complex1,t12_complex1]),
    [file(complex1,t133_complex1),interesting(0.61)]).

fof(l41_complex1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k2_numbers)
     => ! [B] : 
          ( m1_subset_1(B,k2_numbers)
         => k2_xcmplx_0(A,B) = k5_arytm_0(k3_real_1(k3_complex1(A),k3_complex1(B)),k3_real_1(k4_complex1(A),k4_complex1(B))) ) ) ),
    inference(mizar_proof,[status(thm)],[d2_xcmplx_0,l12_complex1,l37_complex1,l12_complex1,l38_complex1,t9_complex1]),
    [file(complex1,l41_complex1),interesting(0.57)]).

fof(t28_complex1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k1_numbers)
     => ! [B] : 
          ( m1_subset_1(B,k1_numbers)
         => ( k3_complex1(k2_xcmplx_0(A,k3_xcmplx_0(B,k7_complex1))) = A
            & k4_complex1(k2_xcmplx_0(A,k3_xcmplx_0(B,k7_complex1))) = B ) ) ) ),
    inference(mizar_proof,[status(thm)],[l47_complex1,l12_complex1]),
    [file(complex1,t28_complex1),interesting(0.56)]).

fof(t148_complex1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ( ~ ( A != B
                & r1_xreal_0(k17_complex1(k6_xcmplx_0(A,B)),0) )
            & ~ ( ~ r1_xreal_0(k17_complex1(k6_xcmplx_0(A,B)),0)
                & A = B ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t132_complex1,t147_complex1,t147_complex1]),
    [file(complex1,t148_complex1),interesting(0.56)]).

fof(t159_complex1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => k1_square_1(A,B) = k7_xcmplx_0(k6_xcmplx_0(k2_xcmplx_0(A,B),k17_complex1(k6_xcmplx_0(A,B))),2) ) ) ),
    inference(mizar_proof,[status(thm)],[t50_xreal_1,l180_complex1,t129_complex1,d1_square_1,t50_xreal_1,d1_square_1,t129_complex1]),
    [file(complex1,t159_complex1),interesting(0.56)]).

fof(t160_complex1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => k2_square_1(A,B) = k7_xcmplx_0(k2_xcmplx_0(k2_xcmplx_0(A,B),k17_complex1(k6_xcmplx_0(A,B))),2) ) ) ),
    inference(mizar_proof,[status(thm)],[t50_xreal_1,d2_square_1,t129_complex1,t50_xreal_1,d2_square_1,t129_complex1,l180_complex1]),
    [file(complex1,t160_complex1),interesting(0.56)]).

fof(l39_complex1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k2_numbers)
     => ! [B] : 
          ( m1_subset_1(B,k2_numbers)
         => ! [C] : 
              ( m1_subset_1(C,k2_numbers)
             => ( C = k3_xcmplx_0(A,B)
               => k3_complex1(C) = k5_real_1(k4_real_1(k3_complex1(A),k3_complex1(B)),k4_real_1(k4_complex1(A),k4_complex1(B))) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d5_xcmplx_0,l12_complex1,l12_complex1,l12_complex1,l34_complex1,l36_complex1,l35_complex1,l36_complex1]),
    [file(complex1,l39_complex1),interesting(0.50)]).

fof(l40_complex1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k2_numbers)
     => ! [B] : 
          ( m1_subset_1(B,k2_numbers)
         => ! [C] : 
              ( m1_subset_1(C,k2_numbers)
             => ( C = k3_xcmplx_0(A,B)
               => k4_complex1(C) = k3_real_1(k4_real_1(k3_complex1(A),k4_complex1(B)),k4_real_1(k4_complex1(A),k3_complex1(B))) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d5_xcmplx_0,l12_complex1,l12_complex1,l12_complex1,l34_complex1,l36_complex1,l36_complex1]),
    [file(complex1,l40_complex1),interesting(0.50)]).

fof(l43_complex1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ( k3_complex1(k3_xcmplx_0(A,B)) = k5_real_1(k4_real_1(k3_complex1(A),k3_complex1(B)),k4_real_1(k4_complex1(A),k4_complex1(B)))
            & k4_complex1(k3_xcmplx_0(A,B)) = k3_real_1(k4_real_1(k3_complex1(A),k4_complex1(B)),k4_real_1(k3_complex1(B),k4_complex1(A))) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d2_xcmplx_0,l42_complex1,l12_complex1]),
    [file(complex1,l43_complex1),interesting(0.46)]).

fof(t24_complex1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ( k3_complex1(k3_xcmplx_0(A,B)) = k5_real_1(k4_real_1(k3_complex1(A),k3_complex1(B)),k4_real_1(k4_complex1(A),k4_complex1(B)))
            & k4_complex1(k3_xcmplx_0(A,B)) = k3_real_1(k4_real_1(k3_complex1(A),k4_complex1(B)),k4_real_1(k3_complex1(B),k4_complex1(A))) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d2_xcmplx_0,l42_complex1,l12_complex1]),
    [file(complex1,t24_complex1),interesting(0.45)]).

fof(t64_complex1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ( k3_complex1(k5_xcmplx_0(A)) = k6_real_1(k3_complex1(A),k3_real_1(k7_square_1(k3_complex1(A)),k7_square_1(k4_complex1(A))))
        & k4_complex1(k5_xcmplx_0(A)) = k6_real_1(k1_real_1(k4_complex1(A)),k3_real_1(k7_square_1(k3_complex1(A)),k7_square_1(k4_complex1(A)))) ) ) ),
    inference(mizar_proof,[status(thm)],[d2_xcmplx_0,d13_complex1,t28_complex1]),
    [file(complex1,t64_complex1),interesting(0.40)]).

fof(t31_complex1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ( ( k3_complex1(A) = 0
              & k3_complex1(B) = 0 )
           => ( k3_complex1(k3_xcmplx_0(A,B)) = k1_real_1(k4_real_1(k4_complex1(A),k4_complex1(B)))
              & k4_complex1(k3_xcmplx_0(A,B)) = 0 ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t24_complex1,t24_complex1]),
    [file(complex1,t31_complex1),interesting(0.40)]).

fof(t128_complex1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k2_numbers)
     => ( k3_complex1(k11_complex1(A,k15_complex1(A))) = 0
        & k4_complex1(k11_complex1(A,k15_complex1(A))) = k4_real_1(2,k4_complex1(A)) ) ) ),
    inference(mizar_proof,[status(thm)],[t48_complex1,t112_complex1,t48_complex1,t112_complex1]),
    [file(complex1,t128_complex1),interesting(0.40)]).

fof(t80_complex1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k2_numbers)
     => ( k3_complex1(A) = 0
       => ( k4_complex1(A) = 0
          | ( k3_complex1(k12_complex1(A)) = 0
            & k4_complex1(k12_complex1(A)) = k1_real_1(k2_real_1(k4_complex1(A))) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t64_complex1,t64_complex1,t188_xcmplx_1,t92_xcmplx_1,t217_xcmplx_1]),
    [file(complex1,t80_complex1),interesting(0.38)]).

fof(l42_complex1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k2_numbers)
     => ! [B] : 
          ( m1_subset_1(B,k2_numbers)
         => k3_xcmplx_0(A,B) = k5_arytm_0(k5_real_1(k4_real_1(k3_complex1(A),k3_complex1(B)),k4_real_1(k4_complex1(A),k4_complex1(B))),k3_real_1(k4_real_1(k3_complex1(A),k4_complex1(B)),k4_real_1(k3_complex1(B),k4_complex1(A)))) ) ) ),
    inference(mizar_proof,[status(thm)],[d2_xcmplx_0,l12_complex1,l39_complex1,l12_complex1,l40_complex1,t9_complex1]),
    [file(complex1,l42_complex1),interesting(0.36)]).

fof(t126_complex1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k2_numbers)
     => ( k3_complex1(k9_complex1(A,k15_complex1(A))) = k3_real_1(k7_square_1(k3_complex1(A)),k7_square_1(k4_complex1(A)))
        & k4_complex1(k9_complex1(A,k15_complex1(A))) = 0 ) ) ),
    inference(mizar_proof,[status(thm)],[t24_complex1,t112_complex1,t112_complex1,t24_complex1,t112_complex1,t112_complex1]),
    [file(complex1,t126_complex1),interesting(0.35)]).

fof(t127_complex1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k2_numbers)
     => ( k3_complex1(k8_complex1(A,k15_complex1(A))) = k4_real_1(2,k3_complex1(A))
        & k4_complex1(k8_complex1(A,k15_complex1(A))) = 0 ) ) ),
    inference(mizar_proof,[status(thm)],[t19_complex1,t112_complex1,t19_complex1,t112_complex1]),
    [file(complex1,t127_complex1),interesting(0.35)]).

fof(t32_complex1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k2_numbers)
     => ( k3_complex1(k9_complex1(A,A)) = k5_real_1(k7_square_1(k3_complex1(A)),k7_square_1(k4_complex1(A)))
        & k4_complex1(k9_complex1(A,A)) = k4_real_1(2,k4_real_1(k3_complex1(A),k4_complex1(A))) ) ) ),
    inference(mizar_proof,[status(thm)],[t24_complex1]),
    [file(complex1,t32_complex1),interesting(0.24)]).

fof(t100_complex1,theorem,(
    $true ),
    file(complex1,t100_complex1),
    [interesting(0.00)]).

fof(t101_complex1,theorem,(
    $true ),
    file(complex1,t101_complex1),
    [interesting(0.00)]).

fof(t102_complex1,theorem,(
    $true ),
    file(complex1,t102_complex1),
    [interesting(0.00)]).

fof(t103_complex1,theorem,(
    $true ),
    file(complex1,t103_complex1),
    [interesting(0.00)]).

fof(t104_complex1,theorem,(
    $true ),
    file(complex1,t104_complex1),
    [interesting(0.00)]).

fof(t105_complex1,theorem,(
    $true ),
    file(complex1,t105_complex1),
    [interesting(0.00)]).

fof(t106_complex1,theorem,(
    $true ),
    file(complex1,t106_complex1),
    [interesting(0.00)]).

fof(t107_complex1,theorem,(
    $true ),
    file(complex1,t107_complex1),
    [interesting(0.00)]).

fof(t108_complex1,theorem,(
    $true ),
    file(complex1,t108_complex1),
    [interesting(0.00)]).

fof(d2_xcmplx_0,definition,(
    ! [A] : 
      ( v1_xcmplx_0(A)
    <=> r2_hidden(A,k2_numbers) ) ),
    file(xcmplx_0,d2_xcmplx_0),
    [interesting(0.00)]).

fof(d13_complex1,definition,(
    ! [A] : 
      ( m1_subset_1(A,k2_numbers)
     => k12_complex1(A) = k2_xcmplx_0(k6_real_1(k3_complex1(A),k3_real_1(k7_square_1(k3_complex1(A)),k7_square_1(k4_complex1(A)))),k3_xcmplx_0(k6_real_1(k1_real_1(k4_complex1(A)),k3_real_1(k7_square_1(k3_complex1(A)),k7_square_1(k4_complex1(A)))),k7_complex1)) ) ),
    file(complex1,d13_complex1),
    [interesting(0.00)]).

fof(d7_arytm_0,definition,(
    ! [A] : 
      ( m1_subset_1(A,k1_numbers)
     => ! [B] : 
          ( m1_subset_1(B,k1_numbers)
         => ( ( B = 0
             => k5_arytm_0(A,B) = A )
            & ( B != 0
             => k5_arytm_0(A,B) = k5_funct_4(k1_numbers,0,k13_arytm_3,A,B) ) ) ) ) ),
    file(arytm_0,d7_arytm_0),
    [interesting(0.00)]).

fof(d2_complex1,definition,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( ( r2_hidden(A,k1_numbers)
           => ( B = k1_complex1(A)
            <=> B = A ) )
          & ( ~ r2_hidden(A,k1_numbers)
           => ( B = k1_complex1(A)
            <=> ? [C] : 
                  ( v1_funct_1(C)
                  & v1_funct_2(C,2,k1_numbers)
                  & m2_relset_1(C,2,k1_numbers)
                  & A = C
                  & B = k1_funct_1(C,0) ) ) ) ) ) ),
    file(complex1,d2_complex1),
    [interesting(0.00)]).

fof(d4_ordinal2,definition,(
    k4_ordinal2 = k1_ordinal1(k1_xboole_0) ),
    file(ordinal2,d4_ordinal2),
    [interesting(0.00)]).

fof(l1_complex1,theorem,(
    k13_arytm_3 = 1 ),
    inference(mizar_proof,[status(thm)],[d4_ordinal2]),
    [file(complex1,l1_complex1),interesting(0.00)]).

fof(d1_ordinal1,definition,(
    ! [A] : k1_ordinal1(A) = k2_xboole_0(A,k1_tarski(A)) ),
    file(ordinal1,d1_ordinal1),
    [interesting(0.00)]).

fof(t41_enumset1,theorem,(
    ! [A,B] : k2_tarski(A,B) = k2_xboole_0(k1_tarski(A),k1_tarski(B)) ),
    file(enumset1,t41_enumset1),
    [interesting(0.00)]).

fof(l2_complex1,theorem,(
    2 = k2_tarski(0,k13_arytm_3) ),
    inference(mizar_proof,[status(thm)],[d1_ordinal1,d1_ordinal1,l1_complex1,t41_enumset1]),
    [file(complex1,l2_complex1),interesting(0.00)]).

fof(t10_arytm_0,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k1_numbers)
     => ! [B] : 
          ( m1_subset_1(B,k1_numbers)
         => ~ r2_hidden(k5_funct_4(k1_numbers,0,k13_arytm_3,A,B),k1_numbers) ) ) ),
    file(arytm_0,t10_arytm_0),
    [interesting(0.00)]).

fof(t66_funct_4,theorem,(
    ! [A,B,C,D] : 
      ( A != B
     => ( k1_funct_1(k4_funct_4(A,B,C,D),A) = C
        & k1_funct_1(k4_funct_4(A,B,C,D),B) = D ) ) ),
    file(funct_4,t66_funct_4),
    [interesting(0.00)]).

fof(d3_complex1,definition,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( ( r2_hidden(A,k1_numbers)
           => ( B = k2_complex1(A)
            <=> B = 0 ) )
          & ( ~ r2_hidden(A,k1_numbers)
           => ( B = k2_complex1(A)
            <=> ? [C] : 
                  ( v1_funct_1(C)
                  & v1_funct_2(C,2,k1_numbers)
                  & m2_relset_1(C,2,k1_numbers)
                  & A = C
                  & B = k1_funct_1(C,1) ) ) ) ) ) ),
    file(complex1,d3_complex1),
    [interesting(0.00)]).

fof(l12_complex1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k1_numbers)
     => ! [B] : 
          ( m1_subset_1(B,k1_numbers)
         => ( k3_complex1(k5_arytm_0(A,B)) = A
            & k4_complex1(k5_arytm_0(A,B)) = B ) ) ) ),
    inference(mizar_proof,[status(thm)],[d7_arytm_0,d2_complex1,l1_complex1,d7_arytm_0,l1_complex1,l2_complex1,l1_complex1,t10_arytm_0,t66_funct_4,d2_complex1,d7_arytm_0,d3_complex1,l1_complex1,d7_arytm_0,l1_complex1,l2_complex1,l1_complex1,t10_arytm_0,t66_funct_4,d3_complex1]),
    [file(complex1,l12_complex1),interesting(0.00)]).

fof(d4_xcmplx_0,definition,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( C = k2_xcmplx_0(A,B)
            <=> ? [D] : 
                  ( m1_subset_1(D,k1_numbers)
                  & ? [E] : 
                      ( m1_subset_1(E,k1_numbers)
                      & ? [F] : 
                          ( m1_subset_1(F,k1_numbers)
                          & ? [G] : 
                              ( m1_subset_1(G,k1_numbers)
                              & A = k5_arytm_0(D,E)
                              & B = k5_arytm_0(F,G)
                              & C = k5_arytm_0(k1_arytm_0(D,F),k1_arytm_0(E,G)) ) ) ) ) ) ) ) ),
    file(xcmplx_0,d4_xcmplx_0),
    [interesting(0.00)]).

fof(d1_xreal_0,definition,(
    ! [A] : 
      ( v1_xreal_0(A)
    <=> r2_hidden(A,k1_numbers) ) ),
    file(xreal_0,d1_xreal_0),
    [interesting(0.00)]).

fof(l33_complex1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( m1_subset_1(B,k1_numbers)
         => ! [C] : 
              ( m1_subset_1(C,k1_numbers)
             => ( A = k5_arytm_0(B,C)
               => ( C = 0
                  & A = B ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d1_xreal_0,d7_arytm_0,t10_arytm_0,d7_arytm_0]),
    [file(complex1,l33_complex1),interesting(0.00)]).

fof(t13_arytm_0,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k1_numbers)
     => ! [B] : 
          ( m1_subset_1(B,k1_numbers)
         => ( B = 0
           => k1_arytm_0(A,B) = A ) ) ) ),
    file(arytm_0,t13_arytm_0),
    [interesting(0.00)]).

fof(l34_complex1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k1_numbers)
     => ! [B] : 
          ( m1_subset_1(B,k1_numbers)
         => ! [C] : 
              ( v1_xreal_0(C)
             => ! [D] : 
                  ( v1_xreal_0(D)
                 => ( ( A = C
                      & B = D )
                   => k1_arytm_0(A,B) = k2_xcmplx_0(C,D) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d4_xcmplx_0,l33_complex1,l33_complex1,t13_arytm_0,d7_arytm_0]),
    [file(complex1,l34_complex1),interesting(0.00)]).

fof(d2_tarski,definition,(
    ! [A,B,C] : 
      ( C = k2_tarski(A,B)
    <=> ! [D] : 
          ( r2_hidden(D,C)
        <=> ( D = A
            | D = B ) ) ) ),
    file(tarski,d2_tarski),
    [interesting(0.00)]).

fof(t7_funct_2,theorem,(
    ! [A,B,C,D] : 
      ( ( v1_funct_1(D)
        & v1_funct_2(D,A,B)
        & m2_relset_1(D,A,B) )
     => ( r2_hidden(C,A)
       => ( B = k1_xboole_0
          | r2_hidden(k1_funct_1(D,C),B) ) ) ) ),
    file(funct_2,t7_funct_2),
    [interesting(0.00)]).

fof(d1_funct_2,definition,(
    ! [A,B,C] : 
      ( m2_relset_1(C,A,B)
     => ( ( ( B = k1_xboole_0
           => A = k1_xboole_0 )
         => ( v1_funct_2(C,A,B)
          <=> A = k4_relset_1(A,B,C) ) )
        & ( B = k1_xboole_0
         => ( A = k1_xboole_0
            | ( v1_funct_2(C,A,B)
            <=> C = k1_xboole_0 ) ) ) ) ) ),
    file(funct_2,d1_funct_2),
    [interesting(0.00)]).

fof(t69_funct_4,theorem,(
    ! [A,B,C,D,E] : 
      ( ( v1_relat_1(E)
        & v1_funct_1(E) )
     => ( ( k1_relat_1(E) = k2_tarski(A,B)
          & k1_funct_1(E,A) = C
          & k1_funct_1(E,B) = D )
       => E = k4_funct_4(A,B,C,D) ) ) ),
    file(funct_4,t69_funct_4),
    [interesting(0.00)]).

fof(t5_complex1,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,2,k1_numbers)
        & m2_relset_1(A,2,k1_numbers) )
     => ? [B] : 
          ( m1_subset_1(B,k1_numbers)
          & ? [C] : 
              ( m1_subset_1(C,k1_numbers)
              & A = k5_funct_4(k1_numbers,0,1,B,C) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l1_complex1,l2_complex1,d2_tarski,t7_funct_2,l1_complex1,l2_complex1,d1_funct_2,t69_funct_4]),
    [file(complex1,t5_complex1),interesting(0.00)]).

fof(d2_numbers,definition,(
    k2_numbers = k2_xboole_0(k4_xboole_0(k1_funct_2(k2_tarski(0,k13_arytm_3),k1_numbers),a_0_0_numbers),k1_numbers) ),
    file(numbers,d2_numbers),
    [interesting(0.00)]).

fof(d2_xboole_0,definition,(
    ! [A,B,C] : 
      ( C = k2_xboole_0(A,B)
    <=> ! [D] : 
          ( r2_hidden(D,C)
        <=> ( r2_hidden(D,A)
            | r2_hidden(D,B) ) ) ) ),
    file(xboole_0,d2_xboole_0),
    [interesting(0.00)]).

fof(d4_xboole_0,definition,(
    ! [A,B,C] : 
      ( C = k4_xboole_0(A,B)
    <=> ! [D] : 
          ( r2_hidden(D,C)
        <=> ( r2_hidden(D,A)
            & ~ r2_hidden(D,B) ) ) ) ),
    file(xboole_0,d4_xboole_0),
    [interesting(0.00)]).

fof(t11_funct_2,theorem,(
    ! [A,B,C] : 
      ( ( v1_funct_1(C)
        & v1_funct_2(C,A,B)
        & m2_relset_1(C,A,B) )
     => ( ( B = k1_xboole_0
         => A = k1_xboole_0 )
       => r2_hidden(C,k1_funct_2(A,B)) ) ) ),
    file(funct_2,t11_funct_2),
    [interesting(0.00)]).

fof(d5_xcmplx_0,definition,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( C = k3_xcmplx_0(A,B)
            <=> ? [D] : 
                  ( m1_subset_1(D,k1_numbers)
                  & ? [E] : 
                      ( m1_subset_1(E,k1_numbers)
                      & ? [F] : 
                          ( m1_subset_1(F,k1_numbers)
                          & ? [G] : 
                              ( m1_subset_1(G,k1_numbers)
                              & A = k5_arytm_0(D,E)
                              & B = k5_arytm_0(F,G)
                              & C = k5_arytm_0(k1_arytm_0(k2_arytm_0(D,F),k3_arytm_0(k2_arytm_0(E,G))),k1_arytm_0(k2_arytm_0(D,G),k2_arytm_0(E,F))) ) ) ) ) ) ) ) ),
    file(xcmplx_0,d5_xcmplx_0),
    [interesting(0.00)]).

fof(t14_arytm_0,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k1_numbers)
     => ! [B] : 
          ( m1_subset_1(B,k1_numbers)
         => ( B = 0
           => k2_arytm_0(A,B) = 0 ) ) ) ),
    file(arytm_0,t14_arytm_0),
    [interesting(0.00)]).

fof(t17_arytm_0,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k1_numbers)
     => ! [B] : 
          ( m1_subset_1(B,k1_numbers)
         => k2_arytm_0(k3_arytm_0(A),B) = k3_arytm_0(k2_arytm_0(A,B)) ) ) ),
    file(arytm_0,t17_arytm_0),
    [interesting(0.00)]).

fof(l36_complex1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k1_numbers)
     => ! [B] : 
          ( m1_subset_1(B,k1_numbers)
         => ! [C] : 
              ( v1_xreal_0(C)
             => ! [D] : 
                  ( v1_xreal_0(D)
                 => ( ( A = C
                      & B = D )
                   => k2_arytm_0(A,B) = k3_xcmplx_0(C,D) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d5_xcmplx_0,l33_complex1,l33_complex1,t14_arytm_0,t13_arytm_0,t13_arytm_0,t14_arytm_0,t17_arytm_0,d7_arytm_0]),
    [file(complex1,l36_complex1),interesting(0.00)]).

fof(d4_arytm_0,definition,(
    ! [A] : 
      ( m1_subset_1(A,k1_numbers)
     => ! [B] : 
          ( m1_subset_1(B,k1_numbers)
         => ( B = k3_arytm_0(A)
          <=> k1_arytm_0(A,B) = 0 ) ) ) ),
    file(arytm_0,d4_arytm_0),
    [interesting(0.00)]).

fof(t17_complex1,theorem,
    ( k3_complex1(k7_complex1) = 0
    & k4_complex1(k7_complex1) = 1 ),
    inference(mizar_proof,[status(thm)],[l12_complex1]),
    [file(complex1,t17_complex1),interesting(0.00)]).

fof(t92_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => ( A != 0
               => k7_xcmplx_0(B,C) = k7_xcmplx_0(k3_xcmplx_0(B,A),k3_xcmplx_0(C,A)) ) ) ) ) ),
    file(xcmplx_1,t92_xcmplx_1),
    [interesting(0.00)]).

fof(t217_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => k7_xcmplx_0(1,A) = k5_xcmplx_0(A) ) ),
    file(xcmplx_1,t217_xcmplx_1),
    [interesting(0.00)]).

fof(t79_complex1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k2_numbers)
     => ( k4_complex1(A) = 0
       => ( k3_complex1(A) = 0
          | ( k3_complex1(k12_complex1(A)) = k2_real_1(k3_complex1(A))
            & k4_complex1(k12_complex1(A)) = 0 ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t64_complex1,t92_xcmplx_1,t217_xcmplx_1,t64_complex1]),
    [file(complex1,t79_complex1),interesting(0.00)]).

fof(d9_xcmplx_0,definition,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => k7_xcmplx_0(A,B) = k3_xcmplx_0(A,k5_xcmplx_0(B)) ) ) ),
    file(xcmplx_0,d9_xcmplx_0),
    [interesting(0.00)]).

fof(t30_complex1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ( ( k4_complex1(A) = 0
              & k4_complex1(B) = 0 )
           => ( k3_complex1(k3_xcmplx_0(A,B)) = k4_real_1(k3_complex1(A),k3_complex1(B))
              & k4_complex1(k3_xcmplx_0(A,B)) = 0 ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t24_complex1,t24_complex1]),
    [file(complex1,t30_complex1),interesting(0.00)]).

fof(t109_complex1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k2_numbers)
     => ! [B] : 
          ( m1_subset_1(B,k2_numbers)
         => ( ( k4_complex1(A) = 0
              & k4_complex1(B) = 0 )
           => ( k3_complex1(B) = 0
              | ( k3_complex1(k13_complex1(A,B)) = k6_real_1(k3_complex1(A),k3_complex1(B))
                & k4_complex1(k13_complex1(A,B)) = 0 ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t79_complex1,d9_xcmplx_0,t30_complex1,t79_complex1,d9_xcmplx_0,t30_complex1]),
    [file(complex1,t109_complex1),interesting(0.00)]).

fof(t10_complex1,theorem,(
    $true ),
    file(complex1,t10_complex1),
    [interesting(0.00)]).

fof(t188_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => k4_xcmplx_0(k7_xcmplx_0(A,B)) = k7_xcmplx_0(k4_xcmplx_0(A),B) ) ) ),
    file(xcmplx_1,t188_xcmplx_1),
    [interesting(0.00)]).

fof(t110_complex1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k2_numbers)
     => ! [B] : 
          ( m1_subset_1(B,k2_numbers)
         => ( ( k3_complex1(A) = 0
              & k3_complex1(B) = 0 )
           => ( k4_complex1(B) = 0
              | ( k3_complex1(k13_complex1(A,B)) = k6_real_1(k4_complex1(A),k4_complex1(B))
                & k4_complex1(k13_complex1(A,B)) = 0 ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t80_complex1,d9_xcmplx_0,t31_complex1,t80_complex1,d9_xcmplx_0,t31_complex1]),
    [file(complex1,t110_complex1),interesting(0.00)]).

fof(t111_complex1,theorem,(
    $true ),
    file(complex1,t111_complex1),
    [interesting(0.00)]).

fof(l23_complex1,theorem,(
    0 = k5_arytm_0(0,0) ),
    inference(mizar_proof,[status(thm)],[d7_arytm_0]),
    [file(complex1,l23_complex1),interesting(0.00)]).

fof(t12_complex1,theorem,
    ( k3_complex1(0) = 0
    & k4_complex1(0) = 0 ),
    inference(mizar_proof,[status(thm)],[l23_complex1,l12_complex1]),
    [file(complex1,t12_complex1),interesting(0.00)]).

fof(t113_complex1,theorem,(
    k15_complex1(0) = 0 ),
    inference(mizar_proof,[status(thm)],[t12_complex1]),
    [file(complex1,t113_complex1),interesting(0.00)]).

fof(d5_complex1,definition,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ( A = B
          <=> ( k3_complex1(A) = k3_complex1(B)
              & k4_complex1(A) = k4_complex1(B) ) ) ) ) ),
    file(complex1,d5_complex1),
    [interesting(0.00)]).

fof(l24_complex1,theorem,(
    k6_complex1 = k5_arytm_0(1,0) ),
    inference(mizar_proof,[status(thm)],[d7_arytm_0]),
    [file(complex1,l24_complex1),interesting(0.00)]).

fof(t15_complex1,theorem,
    ( k3_complex1(k6_complex1) = 1
    & k4_complex1(k6_complex1) = 0 ),
    inference(mizar_proof,[status(thm)],[l24_complex1,l12_complex1]),
    [file(complex1,t15_complex1),interesting(0.00)]).

fof(t115_complex1,theorem,(
    k15_complex1(k6_complex1) = k6_complex1 ),
    inference(mizar_proof,[status(thm)],[t15_complex1]),
    [file(complex1,t115_complex1),interesting(0.00)]).

fof(l68_complex1,theorem,(
    k10_complex1(k7_complex1) = k2_xcmplx_0(0,k3_xcmplx_0(k1_real_1(1),k7_complex1)) ),
    file(complex1,l68_complex1),
    [interesting(0.00)]).

fof(t117_complex1,theorem,(
    $true ),
    file(complex1,t117_complex1),
    [interesting(0.00)]).

fof(t11_complex1,theorem,(
    $true ),
    file(complex1,t11_complex1),
    [interesting(0.00)]).

fof(d11_complex1,definition,(
    ! [A] : 
      ( m1_subset_1(A,k2_numbers)
     => k10_complex1(A) = k2_xcmplx_0(k1_real_1(k3_complex1(A)),k3_xcmplx_0(k1_real_1(k4_complex1(A)),k7_complex1)) ) ),
    file(complex1,d11_complex1),
    [interesting(0.00)]).

fof(t125_complex1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k2_numbers)
     => ( k3_complex1(A) = 0
       => k15_complex1(A) = k10_complex1(A) ) ) ),
    file(complex1,t125_complex1),
    [interesting(0.00)]).

fof(t48_complex1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k2_numbers)
     => ! [B] : 
          ( m1_subset_1(B,k2_numbers)
         => ( k3_complex1(k11_complex1(A,B)) = k5_real_1(k3_complex1(A),k3_complex1(B))
            & k4_complex1(k11_complex1(A,B)) = k5_real_1(k4_complex1(A),k4_complex1(B)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t28_complex1]),
    [file(complex1,t48_complex1),interesting(0.00)]).

fof(t72_square_1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => r1_xreal_0(0,k5_square_1(A)) ) ),
    file(square_1,t72_square_1),
    [interesting(0.00)]).

fof(t9_xreal_1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ! [C] : 
              ( v1_xreal_0(C)
             => ! [D] : 
                  ( v1_xreal_0(D)
                 => ( ( r1_xreal_0(A,B)
                      & r1_xreal_0(C,D) )
                   => r1_xreal_0(k2_xcmplx_0(A,C),k2_xcmplx_0(B,D)) ) ) ) ) ) ),
    file(xreal_1,t9_xreal_1),
    [interesting(0.00)]).

fof(l5_complex1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k1_numbers)
     => ! [B] : 
          ( m1_subset_1(B,k1_numbers)
         => r1_xreal_0(0,k3_real_1(k7_square_1(A),k7_square_1(B))) ) ) ),
    inference(mizar_proof,[status(thm)],[t72_square_1,t9_xreal_1]),
    [file(complex1,l5_complex1),interesting(0.00)]).

fof(t92_square_1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ( ( r1_xreal_0(0,A)
          & k8_square_1(A) = 0 )
       => A = 0 ) ) ),
    file(square_1,t92_square_1),
    [interesting(0.00)]).

fof(t73_square_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ( k5_square_1(A) = 0
       => A = 0 ) ) ),
    file(square_1,t73_square_1),
    [interesting(0.00)]).

fof(t10_xreal_1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ! [C] : 
              ( v1_xreal_0(C)
             => ! [D] : 
                  ( v1_xreal_0(D)
                 => ~ ( ~ r1_xreal_0(B,A)
                      & r1_xreal_0(C,D)
                      & r1_xreal_0(k2_xcmplx_0(B,D),k2_xcmplx_0(A,C)) ) ) ) ) ) ),
    file(xreal_1,t10_xreal_1),
    [interesting(0.00)]).

fof(t2_complex1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ( k2_xcmplx_0(k5_square_1(A),k5_square_1(B)) = 0
          <=> ( A = 0
              & B = 0 ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t72_square_1,t73_square_1,t10_xreal_1]),
    [file(complex1,t2_complex1),interesting(0.00)]).

fof(d4_square_1,definition,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ( r1_xreal_0(0,A)
       => ! [B] : 
            ( v1_xreal_0(B)
           => ( B = k8_square_1(A)
            <=> ( r1_xreal_0(0,B)
                & k5_square_1(B) = A ) ) ) ) ) ),
    file(square_1,d4_square_1),
    [interesting(0.00)]).

fof(t132_complex1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => r1_xreal_0(0,k17_complex1(A)) ) ),
    inference(mizar_proof,[status(thm)],[l5_complex1,d4_square_1]),
    [file(complex1,t132_complex1),interesting(0.00)]).

fof(t82_square_1,theorem,(
    k9_square_1(0) = 0 ),
    file(square_1,t82_square_1),
    [interesting(0.00)]).

fof(l170_complex1,theorem,(
    k9_square_1(k3_real_1(k7_square_1(0),k7_square_1(0))) = 0 ),
    inference(mizar_proof,[status(thm)],[t82_square_1]),
    [file(complex1,l170_complex1),interesting(0.00)]).

fof(t83_square_1,theorem,(
    k9_square_1(1) = 1 ),
    file(square_1,t83_square_1),
    [interesting(0.00)]).

fof(l176_complex1,theorem,(
    k9_square_1(k3_real_1(k7_square_1(1),k7_square_1(0))) = 1 ),
    inference(mizar_proof,[status(thm)],[t83_square_1]),
    [file(complex1,l176_complex1),interesting(0.00)]).

fof(t134_complex1,theorem,(
    k17_complex1(k6_complex1) = 1 ),
    inference(mizar_proof,[status(thm)],[l176_complex1,t15_complex1]),
    [file(complex1,t134_complex1),interesting(0.00)]).

fof(l178_complex1,theorem,(
    k9_square_1(k3_real_1(k7_square_1(0),k7_square_1(1))) = 1 ),
    inference(mizar_proof,[status(thm)],[t83_square_1]),
    [file(complex1,l178_complex1),interesting(0.00)]).

fof(t135_complex1,theorem,(
    k17_complex1(k7_complex1) = 1 ),
    inference(mizar_proof,[status(thm)],[l178_complex1,t17_complex1]),
    [file(complex1,t135_complex1),interesting(0.00)]).

fof(t89_square_1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ( r1_xreal_0(0,A)
       => k8_square_1(k5_square_1(A)) = A ) ) ),
    file(square_1,t89_square_1),
    [interesting(0.00)]).

fof(t129_complex1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ( r1_xreal_0(0,A)
       => k17_complex1(A) = A ) ) ),
    inference(mizar_proof,[status(thm)],[d1_xreal_0,d3_complex1,d2_complex1,t89_square_1,d2_complex1]),
    [file(complex1,t129_complex1),interesting(0.00)]).

fof(t26_xreal_1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ( r1_xreal_0(A,B)
          <=> r1_xreal_0(k4_xcmplx_0(B),k4_xcmplx_0(A)) ) ) ) ),
    file(xreal_1,t26_xreal_1),
    [interesting(0.00)]).

fof(t90_square_1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ( r1_xreal_0(A,0)
       => k8_square_1(k5_square_1(A)) = k4_xcmplx_0(A) ) ) ),
    file(square_1,t90_square_1),
    [interesting(0.00)]).

fof(t94_square_1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ( ( r1_xreal_0(0,A)
              & r1_xreal_0(A,B) )
           => r1_xreal_0(k8_square_1(A),k8_square_1(B)) ) ) ) ),
    file(square_1,t94_square_1),
    [interesting(0.00)]).

fof(t60_xreal_1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ( ~ ( ~ r1_xreal_0(0,A)
            & r1_xreal_0(k4_xcmplx_0(A),0) )
        & ~ ( ~ r1_xreal_0(k4_xcmplx_0(A),0)
            & r1_xreal_0(0,A) ) ) ) ),
    file(xreal_1,t60_xreal_1),
    [interesting(0.00)]).

fof(t2_xreal_1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ! [C] : 
              ( v1_xreal_0(C)
             => ( ( r1_xreal_0(A,B)
                  & r1_xreal_0(B,C) )
               => r1_xreal_0(A,C) ) ) ) ) ),
    file(xreal_1,t2_xreal_1),
    [interesting(0.00)]).

fof(t21_xreal_1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ! [C] : 
              ( v1_xreal_0(C)
             => ( r1_xreal_0(k2_xcmplx_0(A,B),C)
              <=> r1_xreal_0(A,k6_xcmplx_0(C,B)) ) ) ) ) ),
    file(xreal_1,t21_xreal_1),
    [interesting(0.00)]).

fof(t97_square_1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ( ( r1_xreal_0(0,A)
              & r1_xreal_0(0,B) )
           => k8_square_1(k3_xcmplx_0(A,B)) = k3_xcmplx_0(k8_square_1(A),k8_square_1(B)) ) ) ) ),
    file(square_1,t97_square_1),
    [interesting(0.00)]).

fof(t66_xreal_1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ! [C] : 
              ( v1_xreal_0(C)
             => ( ( r1_xreal_0(A,B)
                  & r1_xreal_0(0,C) )
               => r1_xreal_0(k3_xcmplx_0(A,C),k3_xcmplx_0(B,C)) ) ) ) ) ),
    file(xreal_1,t66_xreal_1),
    [interesting(0.00)]).

fof(t22_xreal_1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ! [C] : 
              ( v1_xreal_0(C)
             => ( r1_xreal_0(A,k2_xcmplx_0(B,C))
              <=> r1_xreal_0(k6_xcmplx_0(A,B),C) ) ) ) ) ),
    file(xreal_1,t22_xreal_1),
    [interesting(0.00)]).

fof(t130_complex1,theorem,(
    k17_complex1(0) = 0 ),
    inference(mizar_proof,[status(thm)],[l170_complex1,t12_complex1]),
    [file(complex1,t130_complex1),interesting(0.00)]).

fof(t14_complex1,theorem,(
    $true ),
    file(complex1,t14_complex1),
    [interesting(0.00)]).

fof(t69_square_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => k5_square_1(k7_xcmplx_0(A,B)) = k7_xcmplx_0(k5_square_1(A),k5_square_1(B)) ) ) ),
    file(square_1,t69_square_1),
    [interesting(0.00)]).

fof(t63_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => k2_xcmplx_0(k7_xcmplx_0(A,B),k7_xcmplx_0(C,B)) = k7_xcmplx_0(k2_xcmplx_0(A,C),B) ) ) ) ),
    file(xcmplx_1,t63_xcmplx_1),
    [interesting(0.00)]).

fof(t99_square_1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ( ( r1_xreal_0(0,A)
              & r1_xreal_0(0,B) )
           => k8_square_1(k7_xcmplx_0(A,B)) = k7_xcmplx_0(k8_square_1(A),k8_square_1(B)) ) ) ) ),
    file(square_1,t99_square_1),
    [interesting(0.00)]).

fof(t50_xreal_1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ( r1_xreal_0(A,B)
           => r1_xreal_0(0,k6_xcmplx_0(B,A)) ) ) ) ),
    file(xreal_1,t50_xreal_1),
    [interesting(0.00)]).

fof(d1_square_1,definition,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ( ( r1_xreal_0(A,B)
             => k1_square_1(A,B) = A )
            & ( ~ r1_xreal_0(A,B)
             => k1_square_1(A,B) = B ) ) ) ) ),
    file(square_1,d1_square_1),
    [interesting(0.00)]).

fof(d2_square_1,definition,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ( ( r1_xreal_0(B,A)
             => k2_square_1(A,B) = A )
            & ( ~ r1_xreal_0(B,A)
             => k2_square_1(A,B) = B ) ) ) ) ),
    file(square_1,d2_square_1),
    [interesting(0.00)]).

fof(t163_complex1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k1_numbers)
     => ! [B] : 
          ( m1_subset_1(B,k1_numbers)
         => ! [C] : 
              ( m1_subset_1(C,k1_numbers)
             => ! [D] : 
                  ( m1_subset_1(D,k1_numbers)
                 => ( k2_xcmplx_0(A,k3_xcmplx_0(B,k7_complex1)) = k2_xcmplx_0(C,k3_xcmplx_0(D,k7_complex1))
                   => ( A = C
                      & B = D ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t28_complex1,t12_complex1]),
    [file(complex1,t163_complex1),interesting(0.00)]).

fof(t16_complex1,theorem,(
    $true ),
    file(complex1,t16_complex1),
    [interesting(0.00)]).

fof(t18_complex1,theorem,(
    $true ),
    file(complex1,t18_complex1),
    [interesting(0.00)]).

fof(t1_complex1,theorem,(
    $true ),
    file(complex1,t1_complex1),
    [interesting(0.00)]).

fof(t20_complex1,theorem,(
    $true ),
    file(complex1,t20_complex1),
    [interesting(0.00)]).

fof(t21_complex1,theorem,(
    $true ),
    file(complex1,t21_complex1),
    [interesting(0.00)]).

fof(t22_complex1,theorem,(
    $true ),
    file(complex1,t22_complex1),
    [interesting(0.00)]).

fof(t23_complex1,theorem,(
    $true ),
    file(complex1,t23_complex1),
    [interesting(0.00)]).

fof(t33_complex1,theorem,(
    $true ),
    file(complex1,t33_complex1),
    [interesting(0.00)]).

fof(t35_complex1,theorem,(
    $true ),
    file(complex1,t35_complex1),
    [interesting(0.00)]).

fof(t36_complex1,theorem,(
    $true ),
    file(complex1,t36_complex1),
    [interesting(0.00)]).

fof(t37_complex1,theorem,(
    k9_complex1(k7_complex1,k7_complex1) = k10_complex1(k6_complex1) ),
    file(complex1,t37_complex1),
    [interesting(0.00)]).

fof(t38_complex1,theorem,(
    $true ),
    file(complex1,t38_complex1),
    [interesting(0.00)]).

fof(t39_complex1,theorem,(
    $true ),
    file(complex1,t39_complex1),
    [interesting(0.00)]).

fof(t3_complex1,theorem,(
    $true ),
    file(complex1,t3_complex1),
    [interesting(0.00)]).

fof(t40_complex1,theorem,(
    $true ),
    file(complex1,t40_complex1),
    [interesting(0.00)]).

fof(t41_complex1,theorem,(
    $true ),
    file(complex1,t41_complex1),
    [interesting(0.00)]).

fof(t42_complex1,theorem,(
    $true ),
    file(complex1,t42_complex1),
    [interesting(0.00)]).

fof(t43_complex1,theorem,(
    $true ),
    file(complex1,t43_complex1),
    [interesting(0.00)]).

fof(t44_complex1,theorem,(
    $true ),
    file(complex1,t44_complex1),
    [interesting(0.00)]).

fof(t45_complex1,theorem,(
    $true ),
    file(complex1,t45_complex1),
    [interesting(0.00)]).

fof(t46_complex1,theorem,(
    $true ),
    file(complex1,t46_complex1),
    [interesting(0.00)]).

fof(t47_complex1,theorem,(
    $true ),
    file(complex1,t47_complex1),
    [interesting(0.00)]).

fof(t49_complex1,theorem,(
    $true ),
    file(complex1,t49_complex1),
    [interesting(0.00)]).

fof(t4_complex1,theorem,(
    $true ),
    file(complex1,t4_complex1),
    [interesting(0.00)]).

fof(t50_complex1,theorem,(
    $true ),
    file(complex1,t50_complex1),
    [interesting(0.00)]).

fof(t51_complex1,theorem,(
    $true ),
    file(complex1,t51_complex1),
    [interesting(0.00)]).

fof(t52_complex1,theorem,(
    $true ),
    file(complex1,t52_complex1),
    [interesting(0.00)]).

fof(t53_complex1,theorem,(
    $true ),
    file(complex1,t53_complex1),
    [interesting(0.00)]).

fof(t54_complex1,theorem,(
    $true ),
    file(complex1,t54_complex1),
    [interesting(0.00)]).

fof(t55_complex1,theorem,(
    $true ),
    file(complex1,t55_complex1),
    [interesting(0.00)]).

fof(t56_complex1,theorem,(
    $true ),
    file(complex1,t56_complex1),
    [interesting(0.00)]).

fof(t57_complex1,theorem,(
    $true ),
    file(complex1,t57_complex1),
    [interesting(0.00)]).

fof(t58_complex1,theorem,(
    $true ),
    file(complex1,t58_complex1),
    [interesting(0.00)]).

fof(t59_complex1,theorem,(
    $true ),
    file(complex1,t59_complex1),
    [interesting(0.00)]).

fof(t60_complex1,theorem,(
    $true ),
    file(complex1,t60_complex1),
    [interesting(0.00)]).

fof(t61_complex1,theorem,(
    $true ),
    file(complex1,t61_complex1),
    [interesting(0.00)]).

fof(t62_complex1,theorem,(
    $true ),
    file(complex1,t62_complex1),
    [interesting(0.00)]).

fof(t63_complex1,theorem,(
    $true ),
    file(complex1,t63_complex1),
    [interesting(0.00)]).

fof(t65_complex1,theorem,(
    $true ),
    file(complex1,t65_complex1),
    [interesting(0.00)]).

fof(t66_complex1,theorem,(
    $true ),
    file(complex1,t66_complex1),
    [interesting(0.00)]).

fof(t67_complex1,theorem,(
    $true ),
    file(complex1,t67_complex1),
    [interesting(0.00)]).

fof(t68_complex1,theorem,(
    $true ),
    file(complex1,t68_complex1),
    [interesting(0.00)]).

fof(t69_complex1,theorem,(
    $true ),
    file(complex1,t69_complex1),
    [interesting(0.00)]).

fof(t6_complex1,theorem,(
    $true ),
    file(complex1,t6_complex1),
    [interesting(0.00)]).

fof(t70_complex1,theorem,(
    $true ),
    file(complex1,t70_complex1),
    [interesting(0.00)]).

fof(t71_complex1,theorem,(
    $true ),
    file(complex1,t71_complex1),
    [interesting(0.00)]).

fof(t72_complex1,theorem,(
    k12_complex1(k7_complex1) = k10_complex1(k7_complex1) ),
    file(complex1,t72_complex1),
    [interesting(0.00)]).

fof(t73_complex1,theorem,(
    $true ),
    file(complex1,t73_complex1),
    [interesting(0.00)]).

fof(t74_complex1,theorem,(
    $true ),
    file(complex1,t74_complex1),
    [interesting(0.00)]).

fof(t75_complex1,theorem,(
    $true ),
    file(complex1,t75_complex1),
    [interesting(0.00)]).

fof(t76_complex1,theorem,(
    $true ),
    file(complex1,t76_complex1),
    [interesting(0.00)]).

fof(t77_complex1,theorem,(
    $true ),
    file(complex1,t77_complex1),
    [interesting(0.00)]).

fof(t78_complex1,theorem,(
    $true ),
    file(complex1,t78_complex1),
    [interesting(0.00)]).

fof(t7_complex1,theorem,(
    $true ),
    file(complex1,t7_complex1),
    [interesting(0.00)]).

fof(t81_complex1,theorem,(
    $true ),
    file(complex1,t81_complex1),
    [interesting(0.00)]).

fof(t82_complex1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k2_numbers)
     => ! [B] : 
          ( m1_subset_1(B,k2_numbers)
         => ( k3_complex1(k13_complex1(A,B)) = k6_real_1(k3_real_1(k4_real_1(k3_complex1(A),k3_complex1(B)),k4_real_1(k4_complex1(A),k4_complex1(B))),k3_real_1(k7_square_1(k3_complex1(B)),k7_square_1(k4_complex1(B))))
            & k4_complex1(k13_complex1(A,B)) = k6_real_1(k5_real_1(k4_real_1(k3_complex1(B),k4_complex1(A)),k4_real_1(k3_complex1(A),k4_complex1(B))),k3_real_1(k7_square_1(k3_complex1(B)),k7_square_1(k4_complex1(B)))) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t28_complex1]),
    [file(complex1,t82_complex1),interesting(0.00)]).

fof(t83_complex1,theorem,(
    $true ),
    file(complex1,t83_complex1),
    [interesting(0.00)]).

fof(t84_complex1,theorem,(
    $true ),
    file(complex1,t84_complex1),
    [interesting(0.00)]).

fof(t85_complex1,theorem,(
    $true ),
    file(complex1,t85_complex1),
    [interesting(0.00)]).

fof(t86_complex1,theorem,(
    $true ),
    file(complex1,t86_complex1),
    [interesting(0.00)]).

fof(t87_complex1,theorem,(
    $true ),
    file(complex1,t87_complex1),
    [interesting(0.00)]).

fof(t88_complex1,theorem,(
    $true ),
    file(complex1,t88_complex1),
    [interesting(0.00)]).

fof(t89_complex1,theorem,(
    $true ),
    file(complex1,t89_complex1),
    [interesting(0.00)]).

fof(t8_complex1,theorem,(
    $true ),
    file(complex1,t8_complex1),
    [interesting(0.00)]).

fof(t90_complex1,theorem,(
    $true ),
    file(complex1,t90_complex1),
    [interesting(0.00)]).

fof(t91_complex1,theorem,(
    $true ),
    file(complex1,t91_complex1),
    [interesting(0.00)]).

fof(t92_complex1,theorem,(
    $true ),
    file(complex1,t92_complex1),
    [interesting(0.00)]).

fof(t93_complex1,theorem,(
    $true ),
    file(complex1,t93_complex1),
    [interesting(0.00)]).

fof(t94_complex1,theorem,(
    $true ),
    file(complex1,t94_complex1),
    [interesting(0.00)]).

fof(t95_complex1,theorem,(
    $true ),
    file(complex1,t95_complex1),
    [interesting(0.00)]).

fof(t96_complex1,theorem,(
    $true ),
    file(complex1,t96_complex1),
    [interesting(0.00)]).

fof(t97_complex1,theorem,(
    $true ),
    file(complex1,t97_complex1),
    [interesting(0.00)]).

fof(t98_complex1,theorem,(
    $true ),
    file(complex1,t98_complex1),
    [interesting(0.00)]).

fof(t99_complex1,theorem,(
    $true ),
    file(complex1,t99_complex1),
    [interesting(0.00)]).