let o be object ; :: thesis: for Inv being Function holds
( (divL (o,Inv)) . 0 = {0_No} & (divR (o,Inv)) . 0 = {} )
let Inv be Function; :: thesis: ( (divL (o,Inv)) . 0 = {0_No} & (divR (o,Inv)) . 0 = {} )
( (divL (o,Inv)) . 0 = L_ ((transitions_of (o,Inv)) . 0) & (divR (o,Inv)) . 0 = R_ ((transitions_of (o,Inv)) . 0) ) by Def5, Def6;
then ( (divL (o,Inv)) . 0 = L_ 1_No & (divR (o,Inv)) . 0 = R_ 1_No ) by Def4;
hence ( (divL (o,Inv)) . 0 = {0_No} & (divR (o,Inv)) . 0 = {} ) ; :: thesis: verum