let S be non empty non void ManySortedSign ; for X being V5() 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 V5() 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 t be Element of (Free (S,X)); ( 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 S1[ 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 S1[x -term ]
by Th21;
A2:
now 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
S1[t] ) holds
S1[o -term p]let o be
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
S1[t] ) holds
S1[o -term p]let p be
Element of
Args (
o,
(Free (S,X)));
( ( for t being Element of (Free (S,X)) st t in rng p holds
S1[t] ) implies S1[o -term p] )assume
for
t being
Element of
(Free (S,X)) st
t in rng p holds
S1[
t]
;
S1[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
S1[
o -term p]
;
verum end;
thus
S1[t]
from MSAFREE5:sch 2(A1, A2); verum