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