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

g . i = k . i

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

for i being Nat st 1 <= i & i <= len g holds
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;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

g . i = k . i

proof

hence
( f = h & g = k )
by A2, A3, A4, FINSEQ_1:14; :: thesis: verum
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;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