let n be Nat; :: thesis: for a, b being non trivial Nat st a <= b holds
( Px (a,n) <= Px (b,n) & Py (a,n) <= Py (b,n) )
let a, b be non trivial Nat; :: thesis: ( a <= b implies ( Px (a,n) <= Px (b,n) & Py (a,n) <= Py (b,n) ) )
assume A1: a <= b ; :: thesis: ( Px (a,n) <= Px (b,n) & Py (a,n) <= Py (b,n) )
defpred S₁[ Nat] means ( Px (a,$1) <= Px (b,$1) & Py (a,$1) <= Py (b,$1) );
( Px (a,0) = 1 & Py (a,0) = 0 & Px (b,0) = 1 & Py (b,0) = 0 ) by HILB10_1:3;
then A2: S₁[ 0 ] ;
A3: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A4: S₁[k] ; :: thesis: S₁[k + 1]
set k1 = k + 1;
A5: ( a * a = a ^2 & b * b = b ^2 ) by SQUARE_1:def 1;
then ( a ^2 >= 1 + 0 & b ^2 >= 1 + 0 ) by NAT_1:13;
then A6: ( (a ^2) -' 1 = (a ^2) - 1 & (b ^2) -' 1 = (b ^2) - 1 ) by XREAL_1:233;
a ^2 <= b ^2 by A5, A1, XREAL_1:66;
then A7: (a ^2) -' 1 <= (b ^2) -' 1 by A6, XREAL_1:9;
( (Px (a,k)) * a <= (Px (b,k)) * b & (Py (a,k)) * ((a ^2) -' 1) <= (Py (b,k)) * ((b ^2) -' 1) ) by A1, A7, A4, XREAL_1:66;
then ( Px (a,(k + 1)) = ((Px (a,k)) * a) + ((Py (a,k)) * ((a ^2) -' 1)) & ((Px (a,k)) * a) + ((Py (a,k)) * ((a ^2) -' 1)) <= ((Px (b,k)) * b) + ((Py (b,k)) * ((b ^2) -' 1)) ) by XREAL_1:7, HILB10_1:6;
hence Px (a,(k + 1)) <= Px (b,(k + 1)) by HILB10_1:6; :: thesis: Py (a,(k + 1)) <= Py (b,(k + 1))
(Py (a,k)) * a <= (Py (b,k)) * b by A1, A4, XREAL_1:66;
then ( Py (a,(k + 1)) = (Px (a,k)) + ((Py (a,k)) * a) & (Px (a,k)) + ((Py (a,k)) * a) <= (Px (b,k)) + ((Py (b,k)) * b) ) by A4, XREAL_1:7, HILB10_1:6;
hence Py (a,(k + 1)) <= Py (b,(k + 1)) by HILB10_1:6; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A2, A3);
hence ( Px (a,n) <= Px (b,n) & Py (a,n) <= Py (b,n) ) ; :: thesis: verum