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