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

now :: thesis: for k being Nat st k in dom (Im (F ^ <*x*>)) holds
(Im (F ^ <*x*>)) . k = ((Im F) ^ <*(Im x)*>) . k

let k be Nat; :: thesis: ( k in dom (Im (F ^ <*x*>)) implies (Im (F ^ <*x*>)) . k = ((Im F) ^ <*(Im x)*>) . k )
assume A5: k in dom (Im (F ^ <*x*>)) ; :: thesis: (Im (F ^ <*x*>)) . k = ((Im F) ^ <*(Im x)*>) . k
then k in dom (F ^ <*x*>) by COMSEQ_3:def 4;
then A6: k in Seg (len (F ^ <*x*>)) by FINSEQ_1:def 3;
then k in Seg ((len F) + (len <*x*>)) by FINSEQ_1:22;
then A7: ( 1 <= k & k <= (len F) + (len <*x*>) ) by FINSEQ_1:1;

now :: thesis: (Im (F ^ <*x*>)) . k = ((Im F) ^ <*(Im x)*>) . k

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

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

thus (Im (F ^ <*x*>)) . k = Im ((F ^ <*x*>) . k) by A5, COMSEQ_3:def 4
.= Im x by A8, FINSEQ_1:42
.= ((Im F) ^ <*(Im x)*>) . ((len (Im F)) + 1) by FINSEQ_1:42
.= ((Im F) ^ <*(Im x)*>) . k by A8, A1, A2, FINSEQ_1:def 3 ; :: thesis: verum

end;

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

k <= (len F) + 1 by A7, FINSEQ_1:39;
then k < (len F) + 1 by A9, XXREAL_0:1;
then ( 1 <= k & k <= len F ) by A6, FINSEQ_1:1, NAT_1:13;
then k in Seg (len F) ;
then A10: k in dom F by FINSEQ_1:def 3;
then A11: k in dom (Im F) by COMSEQ_3:def 4;
thus (Im (F ^ <*x*>)) . k = Im ((F ^ <*x*>) . k) by A5, COMSEQ_3:def 4
.= Im (F . k) by A10, FINSEQ_1:def 7
.= (Im F) . k by A11, COMSEQ_3:def 4
.= ((Im F) ^ <*(Im x)*>) . k by A11, FINSEQ_1:def 7 ; :: thesis: verum

end;

end;

end;

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

end;

hence Im (F ^ <*x*>) = (Im F) ^ <*(Im x)*> by A4, FINSEQ_1:13; :: thesis: verum