take mk ; :: thesis: ex f being FinSequence of SCM-Data-Loc \/ the carrier of S st
( f = x `3_3 & mk = f /. 1 )
take <*mk,r*> ; :: thesis: ( <*mk,r*> = x `3_3 & mk = <*mk,r*> /. 1 )
( 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 & mk = <*mk,r*> /. 1 ) by A1, FINSEQ_4:17; :: thesis: verum