let x, y be Element of F1(); :: thesis: ( x =*=> y & P1[y] implies P1[x] )
given p being RedSequence of the reduction of F1() such that A2: ( p . 1 = x & p . (len p) = y ) ; :: according to REWRITE1:def 3,ABSRED_0:def 3 :: thesis: ( not P1[y] or P1[x] )
assume A0: P1[y] ; :: thesis: P1[x]
defpred S1[ Nat] means ( (len p) - \$1 in dom p implies P1[p . ((len p) - \$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] )
assume B1: ( S1[i] & (len p) - (i + 1) in dom p ) ; :: thesis: P1[p . ((len p) - (i + 1))]
then reconsider k = (len p) - (i + 1) as Element of NAT ;
B4: k >= 0 + 1 by ;
( 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 ;
then [(p . k),(p . (k + 1))] in the reduction of F1() by REWRITE1:def 2;
then reconsider a = p . k, b = p . (k + 1) as Element of F1() by ZFMISC_1:87;
( P1[b] & a ==> b ) by ;
hence P1[p . ((len p) - (i + 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 ( (len p) - 1 is Nat & (len p) - ((len p) - 1) = 1 & 1 in dom p ) by ;
hence P1[x] by A2, A5; :: thesis: verum