let n, m be Nat; :: thesis: for o being object
for p being pair object st n <= m holds
( (sqrtL (p,o)) . n c= (sqrtL (p,o)) . m & (sqrtR (p,o)) . n c= (sqrtR (p,o)) . m )
let o be object ; :: thesis: for p being pair object st n <= m holds
( (sqrtL (p,o)) . n c= (sqrtL (p,o)) . m & (sqrtR (p,o)) . n c= (sqrtR (p,o)) . m )
let p be pair object ; :: thesis: ( n <= m implies ( (sqrtL (p,o)) . n c= (sqrtL (p,o)) . m & (sqrtR (p,o)) . n c= (sqrtR (p,o)) . m ) )
defpred S₁[ Nat] means ( (sqrtL (p,o)) . n c= (sqrtL (p,o)) . (n + $1) & (sqrtR (p,o)) . n c= (sqrtR (p,o)) . (n + $1) );
A1: S₁[ 0 ] ;
A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

set T = transitions_of (p,o);
let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: S₁[k] ; :: thesis: S₁[k + 1]
set nk = n + k;
A4: ( (sqrtL (p,o)) . ((n + k) + 1) = ((transitions_of (p,o)) . ((n + k) + 1)) `1 & (sqrtR (p,o)) . ((n + k) + 1) = ((transitions_of (p,o)) . ((n + k) + 1)) `2 ) by Def4, Def5;
A5: ( (sqrtL (p,o)) . (n + k) = L_ ((transitions_of (p,o)) . (n + k)) & (sqrtR (p,o)) . (n + k) = R_ ((transitions_of (p,o)) . (n + k)) ) by Def4, Def5;
( ((transitions_of (p,o)) . ((n + k) + 1)) `1 = (L_ ((transitions_of (p,o)) . (n + k))) \/ (sqrt (o,(L_ ((transitions_of (p,o)) . (n + k))),(R_ ((transitions_of (p,o)) . (n + k))))) & ((transitions_of (p,o)) . ((n + k) + 1)) `2 = ((R_ ((transitions_of (p,o)) . (n + k))) \/ (sqrt (o,(L_ ((transitions_of (p,o)) . (n + k))),(L_ ((transitions_of (p,o)) . (n + k)))))) \/ (sqrt (o,(R_ ((transitions_of (p,o)) . (n + k))),(R_ ((transitions_of (p,o)) . (n + k))))) ) by Def3;
then ( ((transitions_of (p,o)) . ((n + k) + 1)) `1 = (L_ ((transitions_of (p,o)) . (n + k))) \/ (sqrt (o,(L_ ((transitions_of (p,o)) . (n + k))),(R_ ((transitions_of (p,o)) . (n + k))))) & ((transitions_of (p,o)) . ((n + k) + 1)) `2 = (R_ ((transitions_of (p,o)) . (n + k))) \/ ((sqrt (o,(L_ ((transitions_of (p,o)) . (n + k))),(L_ ((transitions_of (p,o)) . (n + k))))) \/ (sqrt (o,(R_ ((transitions_of (p,o)) . (n + k))),(R_ ((transitions_of (p,o)) . (n + k)))))) ) by XBOOLE_1:4;
then ( L_ ((transitions_of (p,o)) . (n + k)) c= L_ ((transitions_of (p,o)) . ((n + k) + 1)) & R_ ((transitions_of (p,o)) . (n + k)) c= R_ ((transitions_of (p,o)) . ((n + k) + 1)) ) by XBOOLE_1:7;
hence S₁[k + 1] by A4, A5, A3, XBOOLE_1:1; :: thesis: verum

end;

A6: for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A2);
assume n <= m ; :: thesis: ( (sqrtL (p,o)) . n c= (sqrtL (p,o)) . m & (sqrtR (p,o)) . n c= (sqrtR (p,o)) . m )
then reconsider mn = m - n as Nat by NAT_1:21;
m = n + mn ;
hence ( (sqrtL (p,o)) . n c= (sqrtL (p,o)) . m & (sqrtR (p,o)) . n c= (sqrtR (p,o)) . m ) by A6; :: thesis: verum