defpred S1[ Nat] means ( 1 <= \$1 & \$1 <= F3() & F4() . \$1 <> F5() . \$1 );
assume A4: F4() <> F5() ; :: thesis: contradiction
dom F4() = Seg (len F5()) by
.= dom F5() by FINSEQ_1:def 3 ;
then consider x being object such that
A5: x in dom F4() and
A6: F4() . x <> F5() . x by A4;
A7: x in Seg (len F4()) by ;
reconsider x = x as Nat by A5;
A8: 1 <= x by ;
x <= F3() by ;
then A9: ex n being Nat st S1[n] by A6, A8;
consider n being Nat such that
A10: ( S1[n] & ( for k being Nat st S1[k] holds
n <= k ) ) from 0 <> n by A10;
then consider k being Nat such that
A11: n = k + 1 by NAT_1:6;
reconsider k = k as Nat ;
reconsider Gk1 = F5() . (k + 1) as Element of F1() by A3, A10, A11, Lm1;
n <> 1 by A2, A3, A10;
then 1 < n by ;
then A12: 1 <= k by ;
k < n by ;
then A13: k < F3() by ;
then reconsider Fk = F4() . k as Element of F1() by A2, A12, Lm1;
n > k by ;
then F4() . k = F5() . k by ;
then A14: P1[k,Fk,Gk1] by A3, A12, A13;
reconsider Fk1 = F4() . (k + 1) as Element of F1() by A2, A10, A11, Lm1;
P1[k,Fk,Fk1] by A2, A12, A13;
hence contradiction by A1, A10, A11, A12, A13, A14; :: thesis: verum