take r ; :: thesis: ex f being FinSequence of SCM-Data-Loc \/ the carrier of S st
( f = x `3_3 & r = f /. 2 )
take <*mk,r*> ; :: thesis: ( <*mk,r*> = x `3_3 & r = <*mk,r*> /. 2 )
( mk is Element of SCM-Data-Loc \/ the carrier of S & r is Element of SCM-Data-Loc \/ the carrier of S ) by XBOOLE_0:def 3;
hence ( <*mk,r*> = x `3_3 & r = <*mk,r*> /. 2 ) by A1, FINSEQ_4:17; :: thesis: verum