let F1, F2 be FinSequence of the carrier of G; :: thesis: ( len F1 = len F & ( for k being Nat st k in dom F holds
F1 . k = (F /. k) |^ a ) & len F2 = len F & ( for k being Nat st k in dom F holds
F2 . k = (F /. k) |^ a ) implies F1 = F2 )
assume that
A2: len F1 = len F and
A3: for k being Nat st k in dom F holds
F1 . k = (F /. k) |^ a and
A4: len F2 = len F and
A5: for k being Nat st k in dom F holds
F2 . k = (F /. k) |^ a ; :: thesis: F1 = F2
A6: dom F1 = Seg (len F) by A2, FINSEQ_1:def 3;

now :: thesis: for k being Nat st k in dom F1 holds
F1 . k = F2 . k

let k be Nat; :: thesis: ( k in dom F1 implies F1 . k = F2 . k )
assume k in dom F1 ; :: thesis: F1 . k = F2 . k
then A7: k in dom F by A6, FINSEQ_1:def 3;
hence F1 . k = (F /. k) |^ a by A3
.= F2 . k by A5, A7 ;
:: thesis: verum

end;

hence F1 = F2 by A2, A4, FINSEQ_2:9; :: thesis: verum