reconsider mm = m1, m2 = m2, k1 = k1, k2 = k2 as Element of SCM-Data-Loc \/ INT by Th1, XBOOLE_0:def 3;

take m1 ; :: thesis: ex f being FinSequence of SCM-Data-Loc \/ INT st

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

take f = <*mm,m2,k1,k2*>; :: thesis: ( f = x `3_3 & m1 = f /. 1 )

thus f = x `3_3 by A1; :: thesis: m1 = f /. 1

thus m1 = f /. 1 by FINSEQ_4:80; :: thesis: verum

take m1 ; :: thesis: ex f being FinSequence of SCM-Data-Loc \/ INT st

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

take f = <*mm,m2,k1,k2*>; :: thesis: ( f = x `3_3 & m1 = f /. 1 )

thus f = x `3_3 by A1; :: thesis: m1 = f /. 1

thus m1 = f /. 1 by FINSEQ_4:80; :: thesis: verum