let s, t be State of SCMPDS ; :: thesis: s +* (t | SCM-Data-Loc ) is State of SCMPDS
A1: product the Object-Kind of SCMPDS c= sproduct the Object-Kind of SCMPDS by CARD_3:67;
t in product the Object-Kind of SCMPDS ;
hence s +* (t | SCM-Data-Loc ) is State of SCMPDS by A1, CARD_3:69, CARD_3:81; :: thesis: verum