let n be Nat; :: thesis: for o being object
for p being pair object holds
( (sqrtL (p,o)) . (n + 1) = ((sqrtL (p,o)) . n) \/ (sqrt (o,((sqrtL (p,o)) . n),((sqrtR (p,o)) . n))) & (sqrtR (p,o)) . (n + 1) = (((sqrtR (p,o)) . n) \/ (sqrt (o,((sqrtL (p,o)) . n),((sqrtL (p,o)) . n)))) \/ (sqrt (o,((sqrtR (p,o)) . n),((sqrtR (p,o)) . n))) )
let o be object ; :: thesis: for p being pair object holds
( (sqrtL (p,o)) . (n + 1) = ((sqrtL (p,o)) . n) \/ (sqrt (o,((sqrtL (p,o)) . n),((sqrtR (p,o)) . n))) & (sqrtR (p,o)) . (n + 1) = (((sqrtR (p,o)) . n) \/ (sqrt (o,((sqrtL (p,o)) . n),((sqrtL (p,o)) . n)))) \/ (sqrt (o,((sqrtR (p,o)) . n),((sqrtR (p,o)) . n))) )
let p be pair object ; :: thesis: ( (sqrtL (p,o)) . (n + 1) = ((sqrtL (p,o)) . n) \/ (sqrt (o,((sqrtL (p,o)) . n),((sqrtR (p,o)) . n))) & (sqrtR (p,o)) . (n + 1) = (((sqrtR (p,o)) . n) \/ (sqrt (o,((sqrtL (p,o)) . n),((sqrtL (p,o)) . n)))) \/ (sqrt (o,((sqrtR (p,o)) . n),((sqrtR (p,o)) . n))) )
set T = transitions_of (p,o);
A1: ( (sqrtL (p,o)) . (n + 1) = ((transitions_of (p,o)) . (n + 1)) `1 & (sqrtR (p,o)) . (n + 1) = ((transitions_of (p,o)) . (n + 1)) `2 ) by Def4, Def5;
( (sqrtL (p,o)) . n = ((transitions_of (p,o)) . n) `1 & (sqrtR (p,o)) . n = ((transitions_of (p,o)) . n) `2 ) by Def4, Def5;
hence ( (sqrtL (p,o)) . (n + 1) = ((sqrtL (p,o)) . n) \/ (sqrt (o,((sqrtL (p,o)) . n),((sqrtR (p,o)) . n))) & (sqrtR (p,o)) . (n + 1) = (((sqrtR (p,o)) . n) \/ (sqrt (o,((sqrtL (p,o)) . n),((sqrtL (p,o)) . n)))) \/ (sqrt (o,((sqrtR (p,o)) . n),((sqrtR (p,o)) . n))) ) by Def3, A1; :: thesis: verum