let k be odd Element of NAT ; :: thesis: for x being Element of F_Complex st Re x = 0 holds
Re ( . (x,k)) = 0

let x be Element of F_Complex; :: thesis: ( Re x = 0 implies Re ( . (x,k)) = 0 )
assume A1: Re x = 0 ; :: thesis: Re ( . (x,k)) = 0
defpred S1[ Nat] means for k1 being Element of NAT st k1 = \$1 & k1 is odd holds
for x being Element of F_Complex st Re x = 0 holds
Re ( . (x,k1)) = 0 ;
A2: now :: thesis: for k being Nat st ( for n being Nat st n < k holds
S1[n] ) holds
S1[k]
let k be Nat; :: thesis: ( ( for n being Nat st n < k holds
S1[n] ) implies S1[k] )

assume A3: for n being Nat st n < k holds
S1[n] ; :: thesis: S1[k]
now :: thesis: ( ( k = 1 & S1[k] ) or ( k = 0 & S1[k] ) or ( k >= 2 & S1[k] ) )
per cases ( k = 1 or k = 0 or k >= 2 ) by NAT_1:23;
case A4: k = 1 ; :: thesis: S1[k]
now :: thesis: for k1 being Element of NAT st k1 = k & k1 is odd holds
for x being Element of F_Complex st Re x = 0 holds
Re ( . (x,k1)) = 0
let k1 be Element of NAT ; :: thesis: ( k1 = k & k1 is odd implies for x being Element of F_Complex st Re x = 0 holds
Re ( . (x,k1)) = 0 )

assume A5: ( k1 = k & k1 is odd ) ; :: thesis: for x being Element of F_Complex st Re x = 0 holds
Re ( . (x,k1)) = 0

let x be Element of F_Complex; :: thesis: ( Re x = 0 implies Re ( . (x,k1)) = 0 )
assume A6: Re x = 0 ; :: thesis: Re ( . (x,k1)) = 0
reconsider z = 0 as Element of NAT by ORDINAL1:def 12;
1 = 0 + 1 ;
then . (x,1) = ( . (x,z)) * x by GROUP_1:def 7
.= () * x by GROUP_1:def 7
.= x ;
hence Re ( . (x,k1)) = 0 by A6, A5, A4; :: thesis: verum
end;
hence S1[k] ; :: thesis: verum
end;
case k >= 2 ; :: thesis: S1[k]
then reconsider n = k - 2 as Element of NAT by INT_1:5;
reconsider n1 = n + 1 as Element of NAT ;
A7: ( n1 + 1 = k & n + 1 = n1 ) ;
now :: thesis: for k1 being Element of NAT st k1 = k & k1 is odd holds
for x being Element of F_Complex st Re x = 0 holds
Re ( . (x,k1)) = 0
let k1 be Element of NAT ; :: thesis: ( k1 = k & k1 is odd implies for x being Element of F_Complex st Re x = 0 holds
Re ( . (x,k1)) = 0 )

assume A8: ( k1 = k & k1 is odd ) ; :: thesis: for x being Element of F_Complex st Re x = 0 holds
Re ( . (x,k1)) = 0

let x be Element of F_Complex; :: thesis: ( Re x = 0 implies Re ( . (x,k1)) = 0 )
assume A9: Re x = 0 ; :: thesis: Re ( . (x,k1)) = 0
A10: n is odd
proof
consider t being Integer such that
A11: k = (2 * t) + 1 by ;
n = (2 * (t - 1)) + 1 by A11;
hence n is odd ; :: thesis: verum
end;
A12: now :: thesis: not n >= k
assume n >= k ; :: thesis: contradiction
then (k - 2) - k >= k - k by XREAL_1:11;
hence contradiction ; :: thesis: verum
end;
A13: . (x,k1) = ( . (x,n1)) * x by
.= (( . (x,n)) * x) * x by GROUP_1:def 7
.= ( . (x,n)) * (x * x) ;
set z1 = . (x,n);
set z2 = x * x;
A14: Im (x * x) = ((Re x) * (Im x)) + ((Re x) * (Im x)) by COMPLEX1:9
.= 0 by A9 ;
A15: Re ( . (x,n)) = 0 by A10, A12, A3, A9;
thus Re ( . (x,k1)) = ((Re ( . (x,n))) * (Re (x * x))) - ((Im ( . (x,n))) * (Im (x * x))) by
.= 0 by ; :: thesis: verum
end;
hence S1[k] ; :: thesis: verum
end;
end;
end;
hence S1[k] ; :: thesis: verum
end;
for k being Nat holds S1[k] from hence Re ( . (x,k)) = 0 by A1; :: thesis: verum