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

set R = the reduction of F_{1}();

assume the reduction of F_{1}() \/ ( the reduction of F_{1}() ~) reduces x,y
; :: according to REWRITE1:def 4,ABSRED_0:def 7 :: thesis: ( not P_{1}[x] or P_{1}[y] )

then consider p being RedSequence of the reduction of F_{1}() \/ ( the reduction of F_{1}() ~) such that

A2: ( p . 1 = x & p . (len p) = y ) by REWRITE1:def 3;

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

set R = the reduction of F

assume the reduction of F

then consider p being RedSequence of the reduction of F

A2: ( p . 1 = x & p . (len p) = y ) by REWRITE1:def 3;

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 B4: ( (i + 1) + 1 <= len p & i + 1 >= 1 ) by NAT_1:11, FINSEQ_3:25;

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

then B3: [(p . (i + 1)),(p . ((i + 1) + 1))] in the reduction of F_{1}() \/ ( 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;

( [a,b] in the reduction of F_{1}() or [a,b] in the reduction of F_{1}() ~ )
by B3, XBOOLE_0:def 3;

then ( a ==> b or b ==> a ) by RELAT_1:def 7;

then ( P_{1}[a] & a <==> b )
by B1, B4, SEQ_4:134;

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 B4: ( (i + 1) + 1 <= len p & i + 1 >= 1 ) by NAT_1:11, FINSEQ_3:25;

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

then B3: [(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

( [a,b] in the reduction of F

then ( a ==> b or b ==> a ) by RELAT_1:def 7;

then ( 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