let f, g, h, k be FinSequence; :: thesis: ( f ^ g = h ^ k & len f = len h & len g = len k implies ( f = h & g = k ) )
assume that
A1: f ^ g = h ^ k and
A2: len f = len h and
A3: len g = len k ; :: thesis: ( f = h & g = k )
A4: for i being Nat st 1 <= i & i <= len f holds
f . i = h . i

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len f implies f . i = h . i )
assume A5: ( 1 <= i & i <= len f ) ; :: thesis: f . i = h . i
then A6: i in dom h by A2, FINSEQ_3:25;
i in dom f by A5, FINSEQ_3:25;
hence f . i = (f ^ g) . i by FINSEQ_1:def 7
.= h . i by A1, A6, FINSEQ_1:def 7 ;
:: thesis: verum

end;

for i being Nat st 1 <= i & i <= len g holds
g . i = k . i

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len g implies g . i = k . i )
assume A7: ( 1 <= i & i <= len g ) ; :: thesis: g . i = k . i
then A8: i in dom k by A3, FINSEQ_3:25;
i in dom g by A7, FINSEQ_3:25;
hence g . i = (f ^ g) . ((len f) + i) by FINSEQ_1:def 7
.= k . i by A1, A2, A8, FINSEQ_1:def 7 ;
:: thesis: verum

end;

hence ( f = h & g = k ) by A2, A3, A4, FINSEQ_1:14; :: thesis: verum