let C be initialized ConstructorSignature; :: thesis: for t1, t2 being expression of C
for f being valuation of C st f unifies t1,t2 holds
f unifies t2,t1
let t1, t2 be expression of C; :: thesis: for f being valuation of C st f unifies t1,t2 holds
f unifies t2,t1
let f be valuation of C; :: thesis: ( f unifies t1,t2 implies f unifies t2,t1 )
assume t1 at f = t2 at f ; :: according to ABCMIZ_A:def 24 :: thesis: f unifies t2,t1
hence t2 at f = t1 at f ; :: according to ABCMIZ_A:def 24 :: thesis: verum