let C be initialized ConstructorSignature; :: thesis: for t1, t2, t3 being expression of C st t1 matches_with t2 & t2 matches_with t3 holds
t1 matches_with t3
let t1, t2, t3 be expression of C; :: thesis: ( t1 matches_with t2 & t2 matches_with t3 implies t1 matches_with t3 )
given f1 being valuation of C such that A1: t1 = t2 at f1 ; :: according to ABCMIZ_A:def 21 :: thesis: ( not t2 matches_with t3 or t1 matches_with t3 )
given f2 being valuation of C such that A2: t2 = t3 at f2 ; :: according to ABCMIZ_A:def 21 :: thesis: t1 matches_with t3
take f2 at f1 ; :: according to ABCMIZ_A:def 21 :: thesis: t1 = t3 at (f2 at f1)
thus t1 = t3 at (f2 at f1) by A1, A2, ABCMIZ_1:149; :: thesis: verum