deffunc H₁( Element of S) -> Subset of (TS (DTConOSA X)) = ParsedTerms (X,$1);
consider f being Function such that
A1: ( dom f = the carrier of S & ( for d being Element of S holds f . d = H₁(d) ) ) from FUNCT_1:sch 4();
reconsider f = f as ManySortedSet of S by A1, PARTFUN1:def 2, RELAT_1:def 18;
f is order-sorted

proof

let s1, s2 be Element of S; :: according to OSALG_1:def 16 :: thesis: ( not s1 <= s2 or f . s1 c= f . s2 )
assume A2: s1 <= s2 ; :: thesis: f . s1 c= f . s2
thus f . s1 c= f . s2 :: thesis: verum

proof

let x1 be object ; :: according to TARSKI:def 3 :: thesis: ( not x1 in f . s1 or x1 in f . s2 )
assume x1 in f . s1 ; :: thesis: x1 in f . s2
then x1 in ParsedTerms (X,s1) by A1;
then consider a being Element of TS (DTConOSA X) such that
A3: x1 = a and
A4: ( ex s3 being Element of S ex x being object st
( s3 <= s1 & x in X . s3 & a = root-tree [x,s3] ) or ex o being OperSymbol of S st
( [o, the carrier of S] = a . {} & the_result_sort_of o <= s1 ) ) ;
( ex s3 being Element of S ex x being object st
( s3 <= s2 & x in X . s3 & a = root-tree [x,s3] ) or ex o being OperSymbol of S st
( [o, the carrier of S] = a . {} & the_result_sort_of o <= s2 ) )

proof

per cases ( ex s3 being Element of S ex x being object st
( s3 <= s1 & x in X . s3 & a = root-tree [x,s3] ) or ex o being OperSymbol of S st
( [o, the carrier of S] = a . {} & the_result_sort_of o <= s1 ) ) by A4;

suppose ex s3 being Element of S ex x being object st
( s3 <= s1 & x in X . s3 & a = root-tree [x,s3] ) ; :: thesis: ( ex s3 being Element of S ex x being object st
( s3 <= s2 & x in X . s3 & a = root-tree [x,s3] ) or ex o being OperSymbol of S st
( [o, the carrier of S] = a . {} & the_result_sort_of o <= s2 ) )

then consider s3 being Element of S, x being set such that
A5: s3 <= s1 and
A6: x in X . s3 and
A7: a = root-tree [x,s3] ;
thus ( ex s3 being Element of S ex x being object st
( s3 <= s2 & x in X . s3 & a = root-tree [x,s3] ) or ex o being OperSymbol of S st
( [o, the carrier of S] = a . {} & the_result_sort_of o <= s2 ) ) by A2, A5, A6, A7, ORDERS_2:3; :: thesis: verum

end;

suppose A8: ex o being OperSymbol of S st
( [o, the carrier of S] = a . {} & the_result_sort_of o <= s1 ) ; :: thesis: ( ex s3 being Element of S ex x being object st
( s3 <= s2 & x in X . s3 & a = root-tree [x,s3] ) or ex o being OperSymbol of S st
( [o, the carrier of S] = a . {} & the_result_sort_of o <= s2 ) )

reconsider s21 = s2 as Element of S ;
consider o being OperSymbol of S such that
A9: [o, the carrier of S] = a . {} and
A10: the_result_sort_of o <= s1 by A8;
the_result_sort_of o <= s21 by A2, A10, ORDERS_2:3;
hence ( ex s3 being Element of S ex x being object st
( s3 <= s2 & x in X . s3 & a = root-tree [x,s3] ) or ex o being OperSymbol of S st
( [o, the carrier of S] = a . {} & the_result_sort_of o <= s2 ) ) by A9; :: thesis: verum

end;

end;

end;

then x1 in ParsedTerms (X,s2) by A3;
hence x1 in f . s2 by A1; :: thesis: verum

end;

end;

then reconsider f = f as OrderSortedSet of S ;
take f ; :: thesis: for s being Element of S holds f . s = ParsedTerms (X,s)
thus for s being Element of S holds f . s = ParsedTerms (X,s) by A1; :: thesis: verum