let x, y be Element of F1(); :: thesis: ( x =*=> y & P1[x] implies P1[y] )
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[x] or P1[y] )
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 ( (i + 1) + 1 <= len p & i + 1 >= 1 ) by ;
then B2: j + 1 in dom p by SEQ_4:134;
then [(p . (i + 1)),(p . ((i + 1) + 1))] in the reduction of F1() by ;
then reconsider a = p . (i + 1), b = p . ((i + 1) + 1) as Element of F1() by ZFMISC_1:87;
( 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