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

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}[x] or P_{1}[y] )

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

defpred S_{1}[ Nat] means ( $1 + 1 in dom p implies P_{1}[p . ($1 + 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 ( ex i being Nat st len p = 1 + i & len p in dom p ) by NAT_1:10, FINSEQ_5:6;

hence P_{1}[y]
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] )

reconsider j = i as Element of NAT by ORDINAL1:def 12;

assume B1: ( S_{1}[i] & (i + 1) + 1 in dom p )
; :: thesis: P_{1}[p . ((i + 1) + 1)]

then ( (i + 1) + 1 <= len p & i + 1 >= 1 ) by NAT_1:11, FINSEQ_3:25;

then B2: j + 1 in dom p by SEQ_4:134;

then [(p . (i + 1)),(p . ((i + 1) + 1))] in the reduction of F_{1}()
by B1, REWRITE1:def 2;

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

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

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

end;reconsider j = i as Element of NAT by ORDINAL1:def 12;

assume B1: ( S

then ( (i + 1) + 1 <= len p & i + 1 >= 1 ) by NAT_1:11, FINSEQ_3:25;

then B2: j + 1 in dom p by SEQ_4:134;

then [(p . (i + 1)),(p . ((i + 1) + 1))] in the reduction of F

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

( P

hence P

len p >= 0 + 1 by NAT_1:13;

then ( ex i being Nat st len p = 1 + i & len p in dom p ) by NAT_1:10, FINSEQ_5:6;

hence P