take ml ; :: thesis: ex ml being Element of SCM-Data-Loc st
( <*ml*> = x `3_3 & ml = <*ml*> /. 1 )
take ml ; :: thesis: ( <*ml*> = x `3_3 & ml = <*ml*> /. 1 )
thus ( <*ml*> = x `3_3 & ml = <*ml*> /. 1 ) by A1, FINSEQ_4:16; :: thesis: verum