consider m being constructor OperSymbol of C such that
A1: the_result_sort_of m = a_Type C and
A2: ex p being FinSequence of QuasiTerms C st
( len p = len (the_arity_of m) & t = m -trm p ) by Th74;
consider p being FinSequence of QuasiTerms C such that
A3: len p = len (the_arity_of m) and
A4: t = m -trm p by A2;
A5: len (p at f) = len p by Th130;
t at f = m -trm (p at f) by A3, A4, Def60;
hence for b₁ being expression of C, a_Type C st b₁ = t at f holds
b₁ is pure by A1, A3, A5, Th75; :: thesis: verum