take mk ; :: thesis: ex f being FinSequence of SCM-Data-Loc st
( f = x `2 & mk = f /. 1 )
take <*mk*> ; :: thesis: ( <*mk*> = x `2 & mk = <*mk*> /. 1 )
thus ( <*mk*> = x `2 & mk = <*mk*> /. 1 ) by A1, FINSEQ_4:25, MCART_1:7; :: thesis: verum