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;

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

hence
F1 = F2
by A2, A4, FINSEQ_2:9; :: thesis: verumF1 . 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;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