let F2, F3 be FinSequence of bool X; :: thesis: ( len F2 = len F1 & ( for n being Nat st n in dom F2 holds
F2 . n = (F1 . n) ` ) & len F3 = len F1 & ( for n being Nat st n in dom F3 holds
F3 . n = (F1 . n) ` ) implies F2 = F3 )
assume that
A2: len F2 = len F1 and
A3: for n being Nat st n in dom F2 holds
F2 . n = (F1 . n) ` and
A4: len F3 = len F1 and
A5: for n being Nat st n in dom F3 holds
F3 . n = (F1 . n) ` ; :: thesis: F2 = F3
( dom F2 = dom F3 & ( for k being Nat st k in dom F2 holds
F2 . k = F3 . k ) )

proof

thus A6: dom F2 = Seg (len F3) by A2, A4, FINSEQ_1:def 3
.= dom F3 by FINSEQ_1:def 3 ; :: thesis: for k being Nat st k in dom F2 holds
F2 . k = F3 . k
let k be Nat; :: thesis: ( k in dom F2 implies F2 . k = F3 . k )
assume A7: k in dom F2 ; :: thesis: F2 . k = F3 . k
hence F2 . k = (F1 . k) ` by A3
.= F3 . k by A5, A6, A7 ;
:: thesis: verum

end;

hence F2 = F3 by FINSEQ_1:13; :: thesis: verum