let C be initialized ConstructorSignature; :: thesis: for t1, t2 being expression of C st t1,t2 are_unifiable holds
t1,t2 are_weakly-unifiable
let t1, t2 be expression of C; :: thesis: ( t1,t2 are_unifiable implies t1,t2 are_weakly-unifiable )
given f being valuation of C such that A1: f unifies t1,t2 ; :: according to ABCMIZ_A:def 25 :: thesis: t1,t2 are_weakly-unifiable
take g = C idval (variables_in t2); :: according to ABCMIZ_A:def 26 :: thesis: ( variables_in t2 c= dom g & t1,t2 at g are_unifiable )
thus variables_in t2 c= dom g by ABCMIZ_1:131; :: thesis: t1,t2 at g are_unifiable
take f ; :: according to ABCMIZ_A:def 25 :: thesis: f unifies t1,t2 at g
thus f unifies t1,t2 at g by A1, ABCMIZ_1:137; :: thesis: verum