take
ml
; :: thesis: ex f being FinSequence of SCM-Data-Loc st

( f = x `3_3 & ml = f /. 2 )

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

thus ( <*mk,ml*> = x `3_3 & ml = <*mk,ml*> /. 2 ) by A1, FINSEQ_4:17; :: thesis: verum

( f = x `3_3 & ml = f /. 2 )

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

thus ( <*mk,ml*> = x `3_3 & ml = <*mk,ml*> /. 2 ) by A1, FINSEQ_4:17; :: thesis: verum