let S be non empty non void ManySortedSign ; :: thesis: for X being non-empty ManySortedSet of the carrier of S
for t being Element of (Free (S,X)) holds
( deg t <> 0 iff ex o being OperSymbol of S ex p being Element of Args (o,(Free (S,X))) st t = o -term p )
let X be non-empty ManySortedSet of the carrier of S; :: thesis: for t being Element of (Free (S,X)) holds
( deg t <> 0 iff ex o being OperSymbol of S ex p being Element of Args (o,(Free (S,X))) st t = o -term p )
let t be Element of (Free (S,X)); :: thesis: ( deg t <> 0 iff ex o being OperSymbol of S ex p being Element of Args (o,(Free (S,X))) st t = o -term p )
defpred S₁[ Element of (Free (S,X))] means ( deg $1 <> 0 iff ex o being OperSymbol of S ex p being Element of Args (o,(Free (S,X))) st $1 = o -term p );
A1: for s being SortSymbol of S
for x being Element of X . s holds S₁[x -term ] by Th21;

A2: now :: thesis: for o being OperSymbol of S
for p being Element of Args (o,(Free (S,X))) st ( for t being Element of (Free (S,X)) st t in rng p holds
S₁[t] ) holds
S₁[o -term p]

let o be OperSymbol of S; :: thesis: for p being Element of Args (o,(Free (S,X))) st ( for t being Element of (Free (S,X)) st t in rng p holds
S₁[t] ) holds
S₁[o -term p]
let p be Element of Args (o,(Free (S,X))); :: thesis: ( ( for t being Element of (Free (S,X)) st t in rng p holds
S₁[t] ) implies S₁[o -term p] )
assume for t being Element of (Free (S,X)) st t in rng p holds
S₁[t] ; :: thesis: S₁[o -term p]
( [o, the carrier of S] in [: the carrier' of S,{ the carrier of S}:] & {} in dom (o -term p) & (o -term p) . {} = [o, the carrier of S] ) by TREES_1:22, ZFMISC_1:106, TREES_4:def 4;
then {} in (o -term p) " [: the carrier' of S,{ the carrier of S}:] by FUNCT_1:def 7;
then {{}} c= (o -term p) " [: the carrier' of S,{ the carrier of S}:] ;
then ( 1 = card {{}} & card {{}} = Segm (card {{}}) & Segm (card {{}}) c= Segm (deg (o -term p)) ) by CARD_1:11, CARD_1:30;
hence S₁[o -term p] ; :: thesis: verum

end;

thus S₁[t] from MSAFREE5:sch 2(A1, A2); :: thesis: verum