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) |^ (@ (I /. k)) ) & len F2 = len F & ( for k being Nat st k in dom F holds
F2 . k = (F /. k) |^ (@ (I /. k)) ) implies F1 = F2 )
assume that
A6: len F1 = len F and
A7: for k being Nat st k in dom F holds
F1 . k = (F /. k) |^ (@ (I /. k)) ; :: thesis: ( not len F2 = len F or ex k being Nat st
( k in dom F & not F2 . k = (F /. k) |^ (@ (I /. k)) ) or F1 = F2 )
assume that
A8: len F2 = len F and
A9: for k being Nat st k in dom F holds
F2 . k = (F /. k) |^ (@ (I /. k)) ; :: thesis: F1 = F2
A10: dom F1 = Seg (len F) by A6, 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 A11: k in dom F by A10, FINSEQ_1:def 3;
hence F1 . k = (F /. k) |^ (@ (I /. k)) by A7
.= F2 . k by A9, A11 ;
:: thesis: verum

end;

hence F1 = F2 by A6, A8, FINSEQ_2:9; :: thesis: verum