set AL = (((ParsedTerms X) #) * the Arity of S) . o;
set AX = ((ParsedTerms X) * the ResultSort of S) . o;
set D = DTConOSA X;
set O = the carrier' of S;
set rs = the_result_sort_of o;
set RS = the ResultSort of S;
defpred S1[ object , object ] means for p being FinSequence of TS (DTConOSA X) st p = $1 holds
$2 = (OSSym (o,X)) -tree p;
A1:
for x being object st x in (((ParsedTerms X) #) * the Arity of S) . o holds
ex y being object st
( y in ((ParsedTerms X) * the ResultSort of S) . o & S1[x,y] )
proof
let x be
object ;
( x in (((ParsedTerms X) #) * the Arity of S) . o implies ex y being object st
( y in ((ParsedTerms X) * the ResultSort of S) . o & S1[x,y] ) )
assume A2:
x in (((ParsedTerms X) #) * the Arity of S) . o
;
ex y being object st
( y in ((ParsedTerms X) * the ResultSort of S) . o & S1[x,y] )
then reconsider p =
x as
FinSequence of
TS (DTConOSA X) by Th5;
OSSym (
o,
X)
==> roots p
by A2, Th7;
then reconsider a =
(OSSym (o,X)) -tree p as
Element of
TS (DTConOSA X) by DTCONSTR:def 1;
take y =
(OSSym (o,X)) -tree p;
( y in ((ParsedTerms X) * the ResultSort of S) . o & S1[x,y] )
o in the
carrier' of
S
;
then
o in dom ((ParsedTerms X) * the ResultSort of S)
by PARTFUN1:def 2;
then A3:
((ParsedTerms X) * the ResultSort of S) . o =
(ParsedTerms X) . ( the ResultSort of S . o)
by FUNCT_1:12
.=
(ParsedTerms X) . (the_result_sort_of o)
by MSUALG_1:def 2
.=
ParsedTerms (
X,
(the_result_sort_of o))
by Def8
;
a . {} = OSSym (
o,
X)
by TREES_4:def 4;
hence
y in ((ParsedTerms X) * the ResultSort of S) . o
by A3;
S1[x,y]
thus
S1[
x,
y]
;
verum
end;
consider f being Function such that
A4:
( dom f = (((ParsedTerms X) #) * the Arity of S) . o & rng f c= ((ParsedTerms X) * the ResultSort of S) . o & ( for x being object st x in (((ParsedTerms X) #) * the Arity of S) . o holds
S1[x,f . x] ) )
from FUNCT_1:sch 6(A1);
reconsider g = f as Function of ((((ParsedTerms X) #) * the Arity of S) . o),(rng f) by A4, FUNCT_2:1;
reconsider g = g as Function of ((((ParsedTerms X) #) * the Arity of S) . o),(((ParsedTerms X) * the ResultSort of S) . o) by A4, FUNCT_2:2;
take
g
; for p being FinSequence of TS (DTConOSA X) st OSSym (o,X) ==> roots p holds
g . p = (OSSym (o,X)) -tree p
let p be FinSequence of TS (DTConOSA X); ( OSSym (o,X) ==> roots p implies g . p = (OSSym (o,X)) -tree p )
assume
OSSym (o,X) ==> roots p
; g . p = (OSSym (o,X)) -tree p
then
p in (((ParsedTerms X) #) * the Arity of S) . o
by Th7;
hence
g . p = (OSSym (o,X)) -tree p
by A4; verum