let s, t be State of ; :: thesis: s +* (t | SCM-Data-Loc ) is State of
( 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 by CARD_3:69, CARD_3:81; :: thesis: verum