let F be FinSequence of COMPLEX ; :: thesis: for x being Element of COMPLEX holds Re (F ^ <*x*>) = (Re F) ^ <*(Re x)*>
let x be Element of COMPLEX ; :: thesis: Re (F ^ <*x*>) = (Re F) ^ <*(Re x)*>
set F1 = Re (F ^ <*x*>);
set F2 = (Re F) ^ <*(Re x)*>;
A0: dom F = dom (Re F) by COMSEQ_3:def 3;
A1: Seg (len F) = dom F by FINSEQ_1:def 3;
A2: len <*(Re x)*> = 1 by FINSEQ_1:56;
P1: dom (Re (F ^ <*x*>)) = dom (F ^ <*x*>) by COMSEQ_3:def 3
.= Seg ((len F) + (len <*x*>)) by FINSEQ_1:def 7
.= Seg ((len (Re F)) + (len <*x*>)) by A0, A1, FINSEQ_1:def 3
.= Seg ((len (Re F)) + (len <*(Re x)*>)) by A2, FINSEQ_1:56
.= dom ((Re F) ^ <*(Re x)*>) by FINSEQ_1:def 7 ;

now

let k be Nat; :: thesis: ( k in dom (Re (F ^ <*x*>)) implies (Re (F ^ <*x*>)) . k = ((Re F) ^ <*(Re x)*>) . k )
assume P20: k in dom (Re (F ^ <*x*>)) ; :: thesis: (Re (F ^ <*x*>)) . k = ((Re F) ^ <*(Re x)*>) . k
then k in dom (F ^ <*x*>) by COMSEQ_3:def 3;
then P21: k in Seg (len (F ^ <*x*>)) by FINSEQ_1:def 3;
then k in Seg ((len F) + (len <*x*>)) by FINSEQ_1:35;
then P22: ( 1 <= k & k <= (len F) + (len <*x*>) ) by FINSEQ_1:3;

now

per cases ( k = (len F) + 1 or k <> (len F) + 1 ) ;

suppose C1: k = (len F) + 1 ; :: thesis: (Re (F ^ <*x*>)) . k = ((Re F) ^ <*(Re x)*>) . k

thus (Re (F ^ <*x*>)) . k = Re ((F ^ <*x*>) . k) by P20, COMSEQ_3:def 3
.= Re x by FINSEQ_1:59, C1
.= ((Re F) ^ <*(Re x)*>) . ((len (Re F)) + 1) by FINSEQ_1:59
.= ((Re F) ^ <*(Re x)*>) . k by C1, A0, A1, FINSEQ_1:def 3 ; :: thesis: verum

end;

suppose C2: k <> (len F) + 1 ; :: thesis: (Re (F ^ <*x*>)) . k = ((Re F) ^ <*(Re x)*>) . k

k <= (len F) + 1 by P22, FINSEQ_1:56;
then k < (len F) + 1 by C2, XXREAL_0:1;
then ( 1 <= k & k <= len F ) by P21, FINSEQ_1:3, NAT_1:13;
then k in Seg (len F) by FINSEQ_1:3;
then C20: k in dom F by FINSEQ_1:def 3;
then C21: k in dom (Re F) by COMSEQ_3:def 3;
thus (Re (F ^ <*x*>)) . k = Re ((F ^ <*x*>) . k) by P20, COMSEQ_3:def 3
.= Re (F . k) by C20, FINSEQ_1:def 7
.= (Re F) . k by C21, COMSEQ_3:def 3
.= ((Re F) ^ <*(Re x)*>) . k by C21, FINSEQ_1:def 7 ; :: thesis: verum

end;

end;

end;

hence (Re (F ^ <*x*>)) . k = ((Re F) ^ <*(Re x)*>) . k ; :: thesis: verum

end;

hence Re (F ^ <*x*>) = (Re F) ^ <*(Re x)*> by FINSEQ_1:17, P1; :: thesis: verum