let n be Nat; :: thesis: for o being object
for Inv being Function holds
( (divL (o,Inv)) . (n + 1) = (((divL (o,Inv)) . n) \/ (divset (((divL (o,Inv)) . n),o,(R_ o),Inv))) \/ (divset (((divR (o,Inv)) . n),o,(L_ o),Inv)) & (divR (o,Inv)) . (n + 1) = (((divR (o,Inv)) . n) \/ (divset (((divL (o,Inv)) . n),o,(L_ o),Inv))) \/ (divset (((divR (o,Inv)) . n),o,(R_ o),Inv)) )
let o be object ; :: thesis: for Inv being Function holds
( (divL (o,Inv)) . (n + 1) = (((divL (o,Inv)) . n) \/ (divset (((divL (o,Inv)) . n),o,(R_ o),Inv))) \/ (divset (((divR (o,Inv)) . n),o,(L_ o),Inv)) & (divR (o,Inv)) . (n + 1) = (((divR (o,Inv)) . n) \/ (divset (((divL (o,Inv)) . n),o,(L_ o),Inv))) \/ (divset (((divR (o,Inv)) . n),o,(R_ o),Inv)) )
let Inv be Function; :: thesis: ( (divL (o,Inv)) . (n + 1) = (((divL (o,Inv)) . n) \/ (divset (((divL (o,Inv)) . n),o,(R_ o),Inv))) \/ (divset (((divR (o,Inv)) . n),o,(L_ o),Inv)) & (divR (o,Inv)) . (n + 1) = (((divR (o,Inv)) . n) \/ (divset (((divL (o,Inv)) . n),o,(L_ o),Inv))) \/ (divset (((divR (o,Inv)) . n),o,(R_ o),Inv)) )
set T = transitions_of (o,Inv);
A1: ( (divL (o,Inv)) . (n + 1) = ((transitions_of (o,Inv)) . (n + 1)) `1 & (divR (o,Inv)) . (n + 1) = ((transitions_of (o,Inv)) . (n + 1)) `2 ) by Def5, Def6;
( (divL (o,Inv)) . n = ((transitions_of (o,Inv)) . n) `1 & (divR (o,Inv)) . n = ((transitions_of (o,Inv)) . n) `2 ) by Def5, Def6;
hence ( (divL (o,Inv)) . (n + 1) = (((divL (o,Inv)) . n) \/ (divset (((divL (o,Inv)) . n),o,(R_ o),Inv))) \/ (divset (((divR (o,Inv)) . n),o,(L_ o),Inv)) & (divR (o,Inv)) . (n + 1) = (((divR (o,Inv)) . n) \/ (divset (((divL (o,Inv)) . n),o,(L_ o),Inv))) \/ (divset (((divR (o,Inv)) . n),o,(R_ o),Inv)) ) by Def4, A1; :: thesis: verum