take
mk
; :: thesis: ex f being FinSequence of SCM-Data-Loc \/ INT st

( f = x `3_3 & mk = f /. 1 )

take <*mk,r*> ; :: thesis: ( <*mk,r*> = x `3_3 & mk = <*mk,r*> /. 1 )

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 & mk = <*mk,r*> /. 1 ) by A1, FINSEQ_4:17; :: thesis: verum

( f = x `3_3 & mk = f /. 1 )

take <*mk,r*> ; :: thesis: ( <*mk,r*> = x `3_3 & mk = <*mk,r*> /. 1 )

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 & mk = <*mk,r*> /. 1 ) by A1, FINSEQ_4:17; :: thesis: verum