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