let o be object ; :: thesis: for p being pair object holds
( (sqrtL (p,o)) . 0 = L_ p & (sqrtR (p,o)) . 0 = R_ p )
let p be pair object ; :: thesis: ( (sqrtL (p,o)) . 0 = L_ p & (sqrtR (p,o)) . 0 = R_ p )
( (sqrtL (p,o)) . 0 = L_ ((transitions_of (p,o)) . 0) & (sqrtR (p,o)) . 0 = R_ ((transitions_of (p,o)) . 0) ) by Def4, Def5;
hence ( (sqrtL (p,o)) . 0 = L_ p & (sqrtR (p,o)) . 0 = R_ p ) by Def3; :: thesis: verum