let x, y be Element of F₁(); :: thesis: ( x <=*=> y & P₁[x] implies P₁[y] )
set R = the reduction of F₁();
assume the reduction of F₁() \/ ( the reduction of F₁() ~) reduces x,y ; :: according to REWRITE1:def 4,ABSRED_0:def 7 :: thesis: ( not P₁[x] or P₁[y] )
then consider p being RedSequence of the reduction of F₁() \/ ( the reduction of F₁() ~) such that
A2: ( p . 1 = x & p . (len p) = y ) by REWRITE1:def 3;
assume A0: P₁[x] ; :: thesis: P₁[y]
defpred S₁[ Nat] means ( $1 + 1 in dom p implies P₁[p . ($1 + 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] )
reconsider j = i as Element of NAT by ORDINAL1:def 12;
assume B1: ( S₁[i] & (i + 1) + 1 in dom p ) ; :: thesis: P₁[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₁() \/ ( the reduction of F₁() ~) by B1, REWRITE1:def 2;
then reconsider a = p . (i + 1), b = p . ((i + 1) + 1) as Element of F₁() by ZFMISC_1:87;
( [a,b] in the reduction of F₁() or [a,b] in the reduction of F₁() ~ ) by B3, XBOOLE_0:def 3;
then ( a ==> b or b ==> a ) by RELAT_1:def 7;
then ( P₁[a] & a <==> b ) by B1, B4, SEQ_4:134;
hence P₁[p . ((i + 1) + 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 ( ex i being Nat st len p = 1 + i & len p in dom p ) by NAT_1:10, FINSEQ_5:6;
hence P₁[y] by A2, A5; :: thesis: verum