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