set AL = (((FreeSort X) # ) * the Arity of S) . o;
set AX = ((FreeSort X) * the ResultSort of S) . o;
set D = DTConMSA X;
set O = the carrier' of S;
set rs = the_result_sort_of o;
set RS = the ResultSort of S;
defpred S1[ set , set ] means for p being FinSequence of TS (DTConMSA X) st p = $1 holds
$2 = (Sym o,X) -tree p;
A1:
for x being set st x in (((FreeSort X) # ) * the Arity of S) . o holds
ex y being set st
( y in ((FreeSort X) * the ResultSort of S) . o & S1[x,y] )
proof
let x be
set ;
:: thesis: ( x in (((FreeSort X) # ) * the Arity of S) . o implies ex y being set st
( y in ((FreeSort X) * the ResultSort of S) . o & S1[x,y] ) )
assume A2:
x in (((FreeSort X) # ) * the Arity of S) . o
;
:: thesis: ex y being set st
( y in ((FreeSort X) * the ResultSort of S) . o & S1[x,y] )
then reconsider p =
x as
FinSequence of
TS (DTConMSA X) by Th8;
take y =
(Sym o,X) -tree p;
:: thesis: ( y in ((FreeSort X) * the ResultSort of S) . o & S1[x,y] )
o in the
carrier' of
S
;
then
o in dom ((FreeSort X) * the ResultSort of S)
by PBOOLE:def 3;
then A3:
((FreeSort X) * the ResultSort of S) . o =
(FreeSort X) . (the ResultSort of S . o)
by FUNCT_1:22
.=
(FreeSort X) . (the_result_sort_of o)
by MSUALG_1:def 7
.=
FreeSort X,
(the_result_sort_of o)
by Def13
;
Sym o,
X ==> roots p
by A2, Th10;
then reconsider a =
(Sym o,X) -tree p as
Element of
TS (DTConMSA X) by DTCONSTR:def 4;
( ex
q being
DTree-yielding FinSequence st
(
p = q &
dom a = tree (doms q) ) &
a . {} = Sym o,
X & ( for
n being
Element of
NAT st
n < len p holds
a | <*n*> = p . (n + 1) ) )
by TREES_4:def 4;
then consider q being
DTree-yielding FinSequence such that A4:
(
p = q &
dom a = tree (doms q) &
a . {} = Sym o,
X & ( for
n being
Element of
NAT st
n < len p holds
a | <*n*> = p . (n + 1) ) )
;
thus
y in ((FreeSort X) * the ResultSort of S) . o
by A3, A4;
:: thesis: S1[x,y]
thus
S1[
x,
y]
;
:: thesis: verum
end;
consider f being Function such that
A5:
( dom f = (((FreeSort X) # ) * the Arity of S) . o & rng f c= ((FreeSort X) * the ResultSort of S) . o & ( for x being set st x in (((FreeSort X) # ) * the Arity of S) . o holds
S1[x,f . x] ) )
from WELLORD2:sch 1(A1);
reconsider g = f as Function of (((FreeSort X) # ) * the Arity of S) . o, rng f by A5, FUNCT_2:3;
reconsider g = g as Function of (((FreeSort X) # ) * the Arity of S) . o,((FreeSort X) * the ResultSort of S) . o by A5, FUNCT_2:4;
take
g
; :: thesis: for p being FinSequence of TS (DTConMSA X) st Sym o,X ==> roots p holds
g . p = (Sym o,X) -tree p
let p be FinSequence of TS (DTConMSA X); :: thesis: ( Sym o,X ==> roots p implies g . p = (Sym o,X) -tree p )
assume
Sym o,X ==> roots p
; :: thesis: g . p = (Sym o,X) -tree p
then
p in (((FreeSort X) # ) * the Arity of S) . o
by Th10;
hence
g . p = (Sym o,X) -tree p
by A5; :: thesis: verum