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 ) )

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

hence
F2 = F3
by FINSEQ_1:13; :: thesis: verum
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;.= 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