let G1, G2 be Group; :: thesis: for phi being Homomorphism of G1,G2
for F1 being FinSequence of the carrier of G1 ex F2 being FinSequence of the carrier of G2 st
( len F1 = len F2 & F2 = phi * F1 & Product F2 = phi . (Product F1) )
let phi be Homomorphism of G1,G2; :: thesis: for F1 being FinSequence of the carrier of G1 ex F2 being FinSequence of the carrier of G2 st
( len F1 = len F2 & F2 = phi * F1 & Product F2 = phi . (Product F1) )
let F1 be FinSequence of the carrier of G1; :: thesis: ex F2 being FinSequence of the carrier of G2 st
( len F1 = len F2 & F2 = phi * F1 & Product F2 = phi . (Product F1) )
set n1 = len F1;
defpred S₁[ object , object ] means ex k being Nat st
( k = $1 & $2 = phi . (F1 . k) );
A1: for k being Nat st k in Seg (len F1) holds
ex x being object st S₁[k,x]

proof

let k be Nat; :: thesis: ( k in Seg (len F1) implies ex x being object st S₁[k,x] )
assume k in Seg (len F1) ; :: thesis: ex x being object st S₁[k,x]
consider x being object such that
B1: x = phi . (F1 . k) ;
take x ; :: thesis: S₁[k,x]
thus S₁[k,x] by B1; :: thesis: verum

end;

consider p being FinSequence such that
A2: dom p = Seg (len F1) and
A3: for k being Nat st k in Seg (len F1) holds
S₁[k,p . k] from FINSEQ_1:sch 1(A1);
A4: len F1 = len p by A2, FINSEQ_1:def 3;
A5: p = phi * F1

proof

B1: len p = len (phi * F1) by A4, FINSEQ_2:33;
for k being Nat st 1 <= k & k <= len p holds
p . k = (phi * F1) . k

proof

let k be Nat; :: thesis: ( 1 <= k & k <= len p implies p . k = (phi * F1) . k )
assume B2: 1 <= k ; :: thesis: ( not k <= len p or p . k = (phi * F1) . k )
assume B3: k <= len p ; :: thesis: p . k = (phi * F1) . k
then k in Seg (len F1) by A4, B2;
then B4: k in dom F1 by FINSEQ_1:def 3;
S₁[k,p . k] by A3, A4, B2, B3, FINSEQ_1:1;
hence p . k = (phi * F1) . k by B4, FUNCT_1:13; :: thesis: verum

end;

hence p = phi * F1 by B1, FINSEQ_1:def 18; :: thesis: verum

end;

then reconsider p = p as FinSequence of the carrier of G2 ;
take F2 = p; :: thesis: ( len F1 = len F2 & F2 = phi * F1 & Product F2 = phi . (Product F1) )
thus len F1 = len F2 by A4; :: thesis: ( F2 = phi * F1 & Product F2 = phi . (Product F1) )
thus F2 = phi * F1 by A5; :: thesis: Product F2 = phi . (Product F1)
thus Product F2 = phi . (Product F1) by A5, ThMappingFrobProdProperty; :: thesis: verum