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

proof

set T = transitions_of (o,Inv);
let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: S₁[k] ; :: thesis: S₁[k + 1]
set nk = n + k;
A4: ( (divL (o,Inv)) . ((n + k) + 1) = ((transitions_of (o,Inv)) . ((n + k) + 1)) `1 & (divR (o,Inv)) . ((n + k) + 1) = ((transitions_of (o,Inv)) . ((n + k) + 1)) `2 ) by Def5, Def6;
A5: ( (divL (o,Inv)) . (n + k) = L_ ((transitions_of (o,Inv)) . (n + k)) & (divR (o,Inv)) . (n + k) = R_ ((transitions_of (o,Inv)) . (n + k)) ) by Def5, Def6;
( ((transitions_of (o,Inv)) . ((n + k) + 1)) `1 = ((L_ ((transitions_of (o,Inv)) . (n + k))) \/ (divset ((L_ ((transitions_of (o,Inv)) . (n + k))),o,(R_ o),Inv))) \/ (divset ((R_ ((transitions_of (o,Inv)) . (n + k))),o,(L_ o),Inv)) & ((transitions_of (o,Inv)) . ((n + k) + 1)) `2 = ((R_ ((transitions_of (o,Inv)) . (n + k))) \/ (divset ((L_ ((transitions_of (o,Inv)) . (n + k))),o,(L_ o),Inv))) \/ (divset ((R_ ((transitions_of (o,Inv)) . (n + k))),o,(R_ o),Inv)) ) by Def4;
then ( ((transitions_of (o,Inv)) . ((n + k) + 1)) `1 = (L_ ((transitions_of (o,Inv)) . (n + k))) \/ ((divset ((L_ ((transitions_of (o,Inv)) . (n + k))),o,(R_ o),Inv)) \/ (divset ((R_ ((transitions_of (o,Inv)) . (n + k))),o,(L_ o),Inv))) & ((transitions_of (o,Inv)) . ((n + k) + 1)) `2 = (R_ ((transitions_of (o,Inv)) . (n + k))) \/ ((divset ((L_ ((transitions_of (o,Inv)) . (n + k))),o,(L_ o),Inv)) \/ (divset ((R_ ((transitions_of (o,Inv)) . (n + k))),o,(R_ o),Inv))) ) by XBOOLE_1:4;
then ( L_ ((transitions_of (o,Inv)) . (n + k)) c= L_ ((transitions_of (o,Inv)) . ((n + k) + 1)) & R_ ((transitions_of (o,Inv)) . (n + k)) c= R_ ((transitions_of (o,Inv)) . ((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: ( (divL (o,Inv)) . n c= (divL (o,Inv)) . m & (divR (o,Inv)) . n c= (divR (o,Inv)) . m )
then reconsider mn = m - n as Nat by NAT_1:21;
m = n + mn ;
hence ( (divL (o,Inv)) . n c= (divL (o,Inv)) . m & (divR (o,Inv)) . n c= (divR (o,Inv)) . m ) by A6; :: thesis: verum