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 18 :: thesis: for b₁ being set holds
( not 1 <= b₁ or not b₁ <= len g1 or g1 . b₁ = g2 . b₁ )
defpred S₁[ Nat] means ( 1 <= $1 & $1 <= len g1 implies g1 . $1 = g2 . $1 );
A9: S₁[ 0 ] ;
A10: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume that
A11: S₁[k] and
1 <= k + 1 and
A12: k + 1 <= len g1 ; :: thesis: g1 . (k + 1) = g2 . (k + 1)

per cases ( k <> 0 or k = 0 ) ;

suppose k <> 0 ; :: thesis: g1 . (k + 1) = g2 . (k + 1)

then A13: 1 <= k by NAT_1:14;
hence g1 . (k + 1) = naming (V,A,(f . ((len f) - k)),(g2 . k)) by A5, A11, A12, NAT_1:13
.= g2 . (k + 1) by A3, A6, A8, A13, A12, NAT_1:13 ;
:: thesis: verum

end;

suppose k = 0 ; :: thesis: g1 . (k + 1) = g2 . (k + 1)

hence g1 . (k + 1) = g2 . (k + 1) by A4, A7; :: thesis: verum

end;

end;

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A9, A10);
hence for b₁ being set holds
( not 1 <= b₁ or not b₁ <= len g1 or g1 . b₁ = g2 . b₁ ) ; :: thesis: verum