reconsider m1 = m1, mm = m2, k1 = k1, k2 = k2 as Element of SCM-Data-Loc \/ INT by Th10, XBOOLE_0:def 3;
take m2 ; :: thesis: ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `2 & m2 = f /. 2 )
take f = <*m1,mm,k1,k2*>; :: thesis: ( f = x `2 & m2 = f /. 2 )
thus f = x `2 by A1, MCART_1:7; :: thesis: m2 = f /. 2
thus m2 = f /. 2 by FINSEQ_4:95; :: thesis: verum