defpred S1[ set ] means ( $1 is expression of F1() implies P1[$1] );
set X = MSVars F1();
set V = (MSVars F1()) (\/) ( the carrier of F1() --> {0});
set S = F1();
set C = F1();
A5: F2() is Term of F1(),((MSVars F1()) (\/) ( the carrier of F1() --> {0})) by MSAFREE3:8;
A6: for s being SortSymbol of F1()
for v being Element of ((MSVars F1()) (\/) ( the carrier of F1() --> {0})) . s holds S1[ root-tree [v,s]]
proof
let s be SortSymbol of F1(); :: thesis: for v being Element of ((MSVars F1()) (\/) ( the carrier of F1() --> {0})) . s holds S1[ root-tree [v,s]]
let v be Element of ((MSVars F1()) (\/) ( the carrier of F1() --> {0})) . s; :: thesis: S1[ root-tree [v,s]]
set t = root-tree [v,s];
assume A7: root-tree [v,s] is expression of F1() ; :: thesis: P1[ root-tree [v,s]]
A8: (root-tree [v,s]) . {} = [v,s] by TREES_4:3;
A9: s in the carrier of F1() ;
A10: ((root-tree [v,s]) . {}) `2 = s by A8;
A11: s <> the carrier of F1() by A9;
per cases ( ex x being variable st root-tree [v,s] = x -term F1() or ex c being constructor OperSymbol of F1() ex p being FinSequence of QuasiTerms F1() st
( len p = len (the_arity_of c) & root-tree [v,s] = c -trm p ) or ex a being expression of F1(), an_Adj F1() st root-tree [v,s] = (non_op F1()) term a or ex a being expression of F1(), an_Adj F1() ex q being expression of F1(), a_Type F1() st root-tree [v,s] = (ast F1()) term (a,q) ) by A7, Th53;
suppose ex c being constructor OperSymbol of F1() ex p being FinSequence of QuasiTerms F1() st
( len p = len (the_arity_of c) & root-tree [v,s] = c -trm p ) ; :: thesis: P1[ root-tree [v,s]]
then consider c being constructor OperSymbol of F1(), p being FinSequence of QuasiTerms F1() such that
A12: len p = len (the_arity_of c) and
A13: root-tree [v,s] = c -trm p ;
root-tree [v,s] = [c, the carrier of F1()] -tree p by A12, A13, Def35;
then (root-tree [v,s]) . {} = [c, the carrier of F1()] by TREES_4:def 4;
hence P1[ root-tree [v,s]] by A10, A11; :: thesis: verum
end;
suppose ex a being expression of F1(), an_Adj F1() st root-tree [v,s] = (non_op F1()) term a ; :: thesis: P1[ root-tree [v,s]]
then consider a being expression of F1(), an_Adj F1() such that
A14: root-tree [v,s] = (non_op F1()) term a ;
A15: the_arity_of (non_op F1()) = <*(an_Adj F1())*> by Def9;
A16: <*(an_Adj F1())*> . 1 = an_Adj F1() ;
len <*(an_Adj F1())*> = 1 by FINSEQ_1:40;
then root-tree [v,s] = [(non_op F1()), the carrier of F1()] -tree <*a*> by A14, A15, A16, Def30;
then (root-tree [v,s]) . {} = [(non_op F1()), the carrier of F1()] by TREES_4:def 4;
hence P1[ root-tree [v,s]] by A10, A11; :: thesis: verum
end;
suppose ex a being expression of F1(), an_Adj F1() ex q being expression of F1(), a_Type F1() st root-tree [v,s] = (ast F1()) term (a,q) ; :: thesis: P1[ root-tree [v,s]]
then consider a being expression of F1(), an_Adj F1(), q being expression of F1(), a_Type F1() such that
A17: root-tree [v,s] = (ast F1()) term (a,q) ;
A18: the_arity_of (ast F1()) = <*(an_Adj F1()),(a_Type F1())*> by Def9;
A19: <*(an_Adj F1()),(a_Type F1())*> . 1 = an_Adj F1() ;
A20: <*(an_Adj F1()),(a_Type F1())*> . 2 = a_Type F1() ;
len <*(an_Adj F1()),(a_Type F1())*> = 2 by FINSEQ_1:44;
then root-tree [v,s] = [(ast F1()), the carrier of F1()] -tree <*a,q*> by A17, A18, A19, A20, Def31;
then (root-tree [v,s]) . {} = [(ast F1()), the carrier of F1()] by TREES_4:def 4;
hence P1[ root-tree [v,s]] by A10, A11; :: thesis: verum
end;
end;
end;
A21: for o being OperSymbol of F1()
for p being ArgumentSeq of Sym (o,((MSVars F1()) (\/) ( the carrier of F1() --> {0}))) st ( for t being Term of F1(),((MSVars F1()) (\/) ( the carrier of F1() --> {0})) st t in rng p holds
S1[t] ) holds
S1[[o, the carrier of F1()] -tree p]
proof
let o be OperSymbol of F1(); :: thesis: for p being ArgumentSeq of Sym (o,((MSVars F1()) (\/) ( the carrier of F1() --> {0}))) st ( for t being Term of F1(),((MSVars F1()) (\/) ( the carrier of F1() --> {0})) st t in rng p holds
S1[t] ) holds
S1[[o, the carrier of F1()] -tree p]
let p be ArgumentSeq of Sym (o,((MSVars F1()) (\/) ( the carrier of F1() --> {0}))); :: thesis: ( ( for t being Term of F1(),((MSVars F1()) (\/) ( the carrier of F1() --> {0})) st t in rng p holds
S1[t] ) implies S1[[o, the carrier of F1()] -tree p] )
assume A22: for t being Term of F1(),((MSVars F1()) (\/) ( the carrier of F1() --> {0})) st t in rng p holds
S1[t] ; :: thesis: S1[[o, the carrier of F1()] -tree p]
set t = [o, the carrier of F1()] -tree p;
assume A23: [o, the carrier of F1()] -tree p is expression of F1() ; :: thesis: P1[[o, the carrier of F1()] -tree p]
per cases ( ex x being variable st [o, the carrier of F1()] -tree p = x -term F1() or ex c being constructor OperSymbol of F1() ex p being FinSequence of QuasiTerms F1() st
( len p = len (the_arity_of c) & [o, the carrier of F1()] -tree p = c -trm p ) or ex a being expression of F1(), an_Adj F1() st [o, the carrier of F1()] -tree p = (non_op F1()) term a or ex a being expression of F1(), an_Adj F1() ex q being expression of F1(), a_Type F1() st [o, the carrier of F1()] -tree p = (ast F1()) term (a,q) ) by A23, Th53;
suppose ex x being variable st [o, the carrier of F1()] -tree p = x -term F1() ; :: thesis: P1[[o, the carrier of F1()] -tree p]
hence P1[[o, the carrier of F1()] -tree p] by A1; :: thesis: verum
end;
suppose ex c being constructor OperSymbol of F1() ex p being FinSequence of QuasiTerms F1() st
( len p = len (the_arity_of c) & [o, the carrier of F1()] -tree p = c -trm p ) ; :: thesis: P1[[o, the carrier of F1()] -tree p]
then consider c being constructor OperSymbol of F1(), q being FinSequence of QuasiTerms F1() such that
A24: len q = len (the_arity_of c) and
A25: [o, the carrier of F1()] -tree p = c -trm q ;
[o, the carrier of F1()] -tree p = [c, the carrier of F1()] -tree q by A24, A25, Def35;
then A26: p = q by TREES_4:15;
now :: thesis: for t being quasi-term of F1() st t in rng q holds
P1[t]
let t be quasi-term of F1(); :: thesis: ( t in rng q implies P1[t] )
t is Term of F1(),((MSVars F1()) (\/) ( the carrier of F1() --> {0})) by MSAFREE3:8;
hence ( t in rng q implies P1[t] ) by A22, A26; :: thesis: verum
end;
hence P1[[o, the carrier of F1()] -tree p] by A2, A24, A25; :: thesis: verum
end;
suppose ex a being expression of F1(), an_Adj F1() st [o, the carrier of F1()] -tree p = (non_op F1()) term a ; :: thesis: P1[[o, the carrier of F1()] -tree p]
then consider a being expression of F1(), an_Adj F1() such that
A27: [o, the carrier of F1()] -tree p = (non_op F1()) term a ;
A28: the_arity_of (non_op F1()) = <*(an_Adj F1())*> by Def9;
A29: <*(an_Adj F1())*> . 1 = an_Adj F1() ;
len <*(an_Adj F1())*> = 1 by FINSEQ_1:40;
then [o, the carrier of F1()] -tree p = [(non_op F1()), the carrier of F1()] -tree <*a*> by A27, A28, A29, Def30;
then A30: p = <*a*> by TREES_4:15;
A31: rng <*a*> = {a} by FINSEQ_1:39;
A32: a in {a} by TARSKI:def 1;
a is Term of F1(),((MSVars F1()) (\/) ( the carrier of F1() --> {0})) by MSAFREE3:8;
hence P1[[o, the carrier of F1()] -tree p] by A3, A22, A27, A30, A31, A32; :: thesis: verum
end;
suppose ex a being expression of F1(), an_Adj F1() ex q being expression of F1(), a_Type F1() st [o, the carrier of F1()] -tree p = (ast F1()) term (a,q) ; :: thesis: P1[[o, the carrier of F1()] -tree p]
then consider a being expression of F1(), an_Adj F1(), q being expression of F1(), a_Type F1() such that
A33: [o, the carrier of F1()] -tree p = (ast F1()) term (a,q) ;
A34: the_arity_of (ast F1()) = <*(an_Adj F1()),(a_Type F1())*> by Def9;
A35: <*(an_Adj F1()),(a_Type F1())*> . 1 = an_Adj F1() ;
A36: <*(an_Adj F1()),(a_Type F1())*> . 2 = a_Type F1() ;
len <*(an_Adj F1()),(a_Type F1())*> = 2 by FINSEQ_1:44;
then [o, the carrier of F1()] -tree p = [(ast F1()), the carrier of F1()] -tree <*a,q*> by A33, A34, A35, A36, Def31;
then A37: p = <*a,q*> by TREES_4:15;
A38: rng <*a,q*> = {a,q} by FINSEQ_2:127;
A39: a in {a,q} by TARSKI:def 2;
A40: q in {a,q} by TARSKI:def 2;
A41: a is Term of F1(),((MSVars F1()) (\/) ( the carrier of F1() --> {0})) by MSAFREE3:8;
A42: q is Term of F1(),((MSVars F1()) (\/) ( the carrier of F1() --> {0})) by MSAFREE3:8;
P1[a] by A22, A37, A38, A39, A41;
hence P1[[o, the carrier of F1()] -tree p] by A4, A22, A33, A37, A38, A40, A42; :: thesis: verum
end;
end;
end;
for t being Term of F1(),((MSVars F1()) (\/) ( the carrier of F1() --> {0})) holds S1[t] from MSATERM:sch 1(A6, A21);
 hence P1[F2()] by A5; :: thesis: verum