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

( 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