let x, y be Element of F₁(); :: thesis: ( x =*=> y & P₁[y] implies P₁[x] )
given p being RedSequence of the reduction of F₁() such that A2: ( p . 1 = x & p . (len p) = y ) ; :: according to REWRITE1:def 3,ABSRED_0:def 3 :: thesis: ( not P₁[y] or P₁[x] )
assume A0: P₁[y] ; :: thesis: P₁[x]
defpred S₁[ Nat] means ( (len p) - $1 in dom p implies P₁[p . ((len p) - $1)] );
A3: S₁[ 0 ] by A0, A2;
A4: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume B1: ( S₁[i] & (len p) - (i + 1) in dom p ) ; :: thesis: P₁[p . ((len p) - (i + 1))]
then reconsider k = (len p) - (i + 1) as Element of NAT ;
B4: k >= 0 + 1 by B1, FINSEQ_3:25;
( i is Element of NAT & k + 1 = (len p) - i ) by ORDINAL1:def 12;
then k + 1 <= len p by IDEA_1:3;
then B2: ( k in dom p & k + 1 in dom p ) by B4, SEQ_4:134;
then [(p . k),(p . (k + 1))] in the reduction of F₁() by REWRITE1:def 2;
then reconsider a = p . k, b = p . (k + 1) as Element of F₁() by ZFMISC_1:87;
( P₁[b] & a ==> b ) by B1, B2, REWRITE1:def 2;
hence P₁[p . ((len p) - (i + 1))] by A1; :: thesis: verum

end;

A5: for i being Nat holds S₁[i] from NAT_1:sch 2(A3, A4);
len p >= 0 + 1 by NAT_1:13;
then ( (len p) - 1 is Nat & (len p) - ((len p) - 1) = 1 & 1 in dom p ) by NAT_1:21, FINSEQ_5:6;
hence P₁[x] by A2, A5; :: thesis: verum