let g1, g2 be FinSequence; :: thesis: ( len g1 = len f & g1 . 1 = naming (V,A,(f . (len f)),a) & ( for n being Nat st 1 <= n & n < len g1 holds

g1 . (n + 1) = naming (V,A,(f . ((len f) - n)),(g1 . n)) ) & len g2 = len f & g2 . 1 = naming (V,A,(f . (len f)),a) & ( for n being Nat st 1 <= n & n < len g2 holds

g2 . (n + 1) = naming (V,A,(f . ((len f) - n)),(g2 . n)) ) implies g1 = g2 )

assume that

A3: len g1 = len f and

A4: g1 . 1 = naming (V,A,(f . (len f)),a) and

A5: for n being Nat st 1 <= n & n < len g1 holds

g1 . (n + 1) = naming (V,A,(f . ((len f) - n)),(g1 . n)) and

A6: len g2 = len f and

A7: g2 . 1 = naming (V,A,(f . (len f)),a) and

A8: for n being Nat st 1 <= n & n < len g2 holds

g2 . (n + 1) = naming (V,A,(f . ((len f) - n)),(g2 . n)) ; :: thesis: g1 = g2

thus len g1 = len g2 by A3, A6; :: according to FINSEQ_1:def 17 :: thesis: for b_{1} being set holds

( not 1 <= b_{1} or not b_{1} <= len g1 or g1 . b_{1} = g2 . b_{1} )

defpred S_{1}[ Nat] means ( 1 <= $1 & $1 <= len g1 implies g1 . $1 = g2 . $1 );

A9: S_{1}[ 0 ]
;

A10: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]
_{1}[k]
from NAT_1:sch 2(A9, A10);

hence for b_{1} being set holds

( not 1 <= b_{1} or not b_{1} <= len g1 or g1 . b_{1} = g2 . b_{1} )
; :: thesis: verum

g1 . (n + 1) = naming (V,A,(f . ((len f) - n)),(g1 . n)) ) & len g2 = len f & g2 . 1 = naming (V,A,(f . (len f)),a) & ( for n being Nat st 1 <= n & n < len g2 holds

g2 . (n + 1) = naming (V,A,(f . ((len f) - n)),(g2 . n)) ) implies g1 = g2 )

assume that

A3: len g1 = len f and

A4: g1 . 1 = naming (V,A,(f . (len f)),a) and

A5: for n being Nat st 1 <= n & n < len g1 holds

g1 . (n + 1) = naming (V,A,(f . ((len f) - n)),(g1 . n)) and

A6: len g2 = len f and

A7: g2 . 1 = naming (V,A,(f . (len f)),a) and

A8: for n being Nat st 1 <= n & n < len g2 holds

g2 . (n + 1) = naming (V,A,(f . ((len f) - n)),(g2 . n)) ; :: thesis: g1 = g2

thus len g1 = len g2 by A3, A6; :: according to FINSEQ_1:def 17 :: thesis: for b

( not 1 <= b

defpred S

A9: S

A10: for k being Nat st S

S

proof

for k being Nat holds S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume that

A11: S_{1}[k]
and

1 <= k + 1 and

A12: k + 1 <= len g1 ; :: thesis: g1 . (k + 1) = g2 . (k + 1)

end;assume that

A11: S

1 <= k + 1 and

A12: k + 1 <= len g1 ; :: thesis: g1 . (k + 1) = g2 . (k + 1)

hence for b

( not 1 <= b