let C be initialized ConstructorSignature; :: thesis: for t1, t2, t being expression of C st t is_a_unification_of t1,t2 holds
( t matches_with t1 & t matches_with t2 )
let t1, t2, t be expression of C; :: thesis: ( t is_a_unification_of t1,t2 implies ( t matches_with t1 & t matches_with t2 ) )
given f being valuation of C such that A1: ( f unifies t1,t2 & t = t1 at f ) ; :: according to ABCMIZ_A:def 27 :: thesis: ( t matches_with t1 & t matches_with t2 )
thus ex f being valuation of C st t = t1 at f by A1; :: according to ABCMIZ_A:def 21 :: thesis: t matches_with t2
take f ; :: according to ABCMIZ_A:def 21 :: thesis: t = t2 at f
thus t = t2 at f by A1; :: thesis: verum