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

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

( f = x `3_3 & k2 = f /. 3 )

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

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

thus k2 = f /. 3 by FINSEQ_4:18; :: thesis: verum

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

( f = x `3_3 & k2 = f /. 3 )

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

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

thus k2 = f /. 3 by FINSEQ_4:18; :: thesis: verum