let C be initialized ConstructorSignature; :: thesis: for T1, T2, T3 being quasi-type of C st T1 matches_with T2 & T2 matches_with T3 holds
T1 matches_with T3
let t1, t2, t3 be quasi-type 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: ( (adjs t2) at f1 c= adjs t1 & (the_base_of t2) at f1 = the_base_of t1 ) ; :: according to ABCMIZ_A:def 23 :: thesis: ( not t2 matches_with t3 or t1 matches_with t3 )
given f2 being valuation of C such that A2: ( (adjs t3) at f2 c= adjs t2 & (the_base_of t3) at f2 = the_base_of t2 ) ; :: according to ABCMIZ_A:def 23 :: thesis: t1 matches_with t3
take f2 at f1 ; :: according to ABCMIZ_A:def 23 :: thesis: ( (adjs t3) at (f2 at f1) c= adjs t1 & (the_base_of t3) at (f2 at f1) = the_base_of t1 )
((adjs t3) at f2) at f1 c= (adjs t2) at f1 by A2, ABCMIZ_1:146;
then ((adjs t3) at f2) at f1 c= adjs t1 by A1;
hence ( (adjs t3) at (f2 at f1) c= adjs t1 & (the_base_of t3) at (f2 at f1) = the_base_of t1 ) by A1, A2, ABCMIZ_1:149, ABCMIZ_1:150; :: thesis: verum