let x, y be Element of F1(); :: thesis: ( x <=*=> y & P1[x] implies P1[y] )
set R = the reduction of F1();
assume the reduction of F1() \/ ( the reduction of F1() ~) reduces x,y ; :: according to REWRITE1:def 4,ABSRED_0:def 7 :: thesis: ( not P1[x] or P1[y] )
then consider p being RedSequence of the reduction of F1() \/ ( the reduction of F1() ~) such that
A2: ( p . 1 = x & p . (len p) = y ) by REWRITE1:def 3;
assume A0: P1[x] ; :: thesis: P1[y]
defpred S1[ Nat] means ( \$1 + 1 in dom p implies P1[p . (\$1 + 1)] );
A3: S1[ 0 ] by A0, A2;
A4: for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be Nat; :: thesis: ( S1[i] implies S1[i + 1] )
reconsider j = i as Element of NAT by ORDINAL1:def 12;
assume B1: ( S1[i] & (i + 1) + 1 in dom p ) ; :: thesis: P1[p . ((i + 1) + 1)]
then B4: ( (i + 1) + 1 <= len p & i + 1 >= 1 ) by ;
then j + 1 in dom p by SEQ_4:134;
then B3: [(p . (i + 1)),(p . ((i + 1) + 1))] in the reduction of F1() \/ ( the reduction of F1() ~) by ;
then reconsider a = p . (i + 1), b = p . ((i + 1) + 1) as Element of F1() by ZFMISC_1:87;
( [a,b] in the reduction of F1() or [a,b] in the reduction of F1() ~ ) by ;
then ( a ==> b or b ==> a ) by RELAT_1:def 7;
then ( P1[a] & a <==> b ) by ;
hence P1[p . ((i + 1) + 1)] by A1; :: thesis: verum
end;
A5: for i being Nat holds S1[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 ;
hence P1[y] by A2, A5; :: thesis: verum