let x, y be Element of F_{1}(); :: thesis: ( x =*=> y & P_{1}[y] implies P_{1}[x] )

given p being RedSequence of the reduction of F_{1}() such that A2:
( p . 1 = x & p . (len p) = y )
; :: according to REWRITE1:def 3,ABSRED_0:def 3 :: thesis: ( not P_{1}[y] or P_{1}[x] )

assume A0: P_{1}[y]
; :: thesis: P_{1}[x]

defpred S_{1}[ Nat] means ( (len p) - $1 in dom p implies P_{1}[p . ((len p) - $1)] );

A3: S_{1}[ 0 ]
by A0, A2;

A4: for i being Nat st S_{1}[i] holds

S_{1}[i + 1]
_{1}[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_{1}[x]
by A2, A5; :: thesis: verum

given p being RedSequence of the reduction of F

assume A0: P

defpred S

A3: S

A4: for i being Nat st S

S

proof

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

assume B1: ( S_{1}[i] & (len p) - (i + 1) in dom p )
; :: thesis: P_{1}[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_{1}()
by REWRITE1:def 2;

then reconsider a = p . k, b = p . (k + 1) as Element of F_{1}() by ZFMISC_1:87;

( P_{1}[b] & a ==> b )
by B1, B2, REWRITE1:def 2;

hence P_{1}[p . ((len p) - (i + 1))]
by A1; :: thesis: verum

end;assume B1: ( S

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

then reconsider a = p . k, b = p . (k + 1) as Element of F

( P

hence P

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