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

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

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

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

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

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

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