let C be initialized standardized ConstructorSignature; :: thesis: for t being expression of C holds
( t is non compound quasi-term of C iff (t . {}) `1 in Vars )
let t be expression of C; :: thesis: ( t is non compound quasi-term of C iff (t . {}) `1 in Vars )
hereby :: thesis: ( (t . {}) `1 in Vars implies t is non compound quasi-term of C )
assume t is non compound quasi-term of C ; :: thesis: (t . {}) `1 in Vars
then consider x being Element of Vars such that
A1: t = x -term C by Th3;
( t . {} = [x,a_Term] & x in Vars ) by A1, TREES_4:3;
hence (t . {}) `1 in Vars ; :: thesis: verum
end;
assume (t . {}) `1 in Vars ; :: thesis: t is non compound quasi-term of C
then ex x being Element of Vars st
( x = (t . {}) `1 & t = x -term C ) by Th17;
hence t is non compound quasi-term of C ; :: thesis: verum