( ex x being Element of Vars st
( e = x -term C & e . {} = [x,a_Term ] ) or ex o being OperSymbol of C st
( e . {} = [o,the carrier of C] & ( o in Constructors or o = * or o = non_op ) ) ) by Th49;
hence e . {} is pair ; :: thesis: verum