sy in [:the carrier' of S,{the carrier of S}:] by Lm5;
then consider o being OperSymbol of S, x2 being Element of {the carrier of S} such that
A1: sy = [o,x2] by DOMAIN_1:9;
A2: x2 = the carrier of S by TARSKI:def 1;
then sy = Sym o,V by A1, MSAFREE:def 11;
hence sy -tree p is Term of S,V by A1, A2, Th1; :: thesis: verum