theorem Th17: :: ABCMIZ_A:17

for C being initialized standardized ConstructorSignature
for e being expression of C st (e . {}) `1 in Vars holds
ex x being Element of Vars st
( x = (e . {}) `1 & e = x -term C )