A5:
FreeMSA F2() = MSAlgebra(# (FreeSort F2()),(FreeOper F2()) #)
by MSAFREE:def 16;
then reconsider f1 = F4(), f2 = F5() as ManySortedFunction of FreeSort F2(),the Sorts of F3() ;
defpred S1[ set , set ] means for s being SortSymbol of F1() st $1 in FreeGen s,F2() holds
P1[s,$2,$1];
A6:
for x being set st x in Union (FreeGen F2()) holds
ex y being set st
( y in Union the Sorts of F3() & S1[x,y] )
proof
let e be
set ;
:: thesis: ( e in Union (FreeGen F2()) implies ex y being set st
( y in Union the Sorts of F3() & S1[e,y] ) )
assume
e in Union (FreeGen F2())
;
:: thesis: ex y being set st
( y in Union the Sorts of F3() & S1[e,y] )
then consider s being
set such that A7:
(
s in dom (FreeGen F2()) &
e in (FreeGen F2()) . s )
by CARD_5:10;
reconsider s =
s as
SortSymbol of
F1()
by A7, PARTFUN1:def 4;
take u =
(F4() . s) . e;
:: thesis: ( u in Union the Sorts of F3() & S1[e,u] )
A8:
e in FreeGen s,
F2()
by A7, MSAFREE:def 18;
f1 . s is
Function of
((FreeSort F2()) . s),
(the Sorts of F3() . s)
;
then A9:
u in the
Sorts of
F3()
. s
by A8, FUNCT_2:7;
dom the
Sorts of
F3()
= the
carrier of
F1()
by PARTFUN1:def 4;
hence
u in Union the
Sorts of
F3()
by A9, CARD_5:10;
:: thesis: S1[e,u]
let s' be
SortSymbol of
F1();
:: thesis: ( e in FreeGen s',F2() implies P1[s',u,e] )
assume A10:
e in FreeGen s',
F2()
;
:: thesis: P1[s',u,e]
then
((FreeSort F2()) . s') /\ ((FreeSort F2()) . s) <> {}
by A8, XBOOLE_0:def 4;
then
(FreeSort F2()) . s' meets (FreeSort F2()) . s
by XBOOLE_0:def 7;
then
s = s'
by MSAFREE:13;
hence
P1[
s',
u,
e]
by A2, A10;
:: thesis: verum
end;
consider G being Function of (Union (FreeGen F2())),(Union the Sorts of F3()) such that
A11:
for e being set st e in Union (FreeGen F2()) holds
S1[e,G . e]
from FUNCT_2:sch 1(A6);
consider R being set such that
A12:
R = { [o,a] where o is Element of the carrier' of F1(), a is Element of Args o,F3() : verum }
;
defpred S2[ set , set ] means for o being OperSymbol of F1()
for a being Element of Args o,F3() st $1 = [o,a] holds
$2 = (Den o,F3()) . a;
A13:
for x being set st x in R holds
ex y being set st
( y in Union the Sorts of F3() & S2[x,y] )
proof
let e be
set ;
:: thesis: ( e in R implies ex y being set st
( y in Union the Sorts of F3() & S2[e,y] ) )
assume
e in R
;
:: thesis: ex y being set st
( y in Union the Sorts of F3() & S2[e,y] )
then consider o being
OperSymbol of
F1(),
a being
Element of
Args o,
F3()
such that A14:
e = [o,a]
by A12;
reconsider u =
(Den o,F3()) . a as
set ;
take
u
;
:: thesis: ( u in Union the Sorts of F3() & S2[e,u] )
u in union (rng the Sorts of F3())
by TARSKI:def 4;
hence
u in Union the
Sorts of
F3()
by CARD_3:def 4;
:: thesis: S2[e,u]
let o' be
OperSymbol of
F1();
:: thesis: for a being Element of Args o',F3() st e = [o',a] holds
u = (Den o',F3()) . alet x' be
Element of
Args o',
F3();
:: thesis: ( e = [o',x'] implies u = (Den o',F3()) . x' )
assume
e = [o',x']
;
:: thesis: u = (Den o',F3()) . x'
then
(
o = o' &
a = x' )
by A14, ZFMISC_1:33;
hence
u = (Den o',F3()) . x'
;
:: thesis: verum
end;
consider H being Function of R,(Union the Sorts of F3()) such that
A15:
for e being set st e in R holds
S2[e,H . e]
from FUNCT_2:sch 1(A13);
deffunc H1( set ) -> Element of Union the Sorts of F3() = G /. $1;
deffunc H2( set , set , set ) -> Element of Union the Sorts of F3() = H /. [$1,$3];
A16:
for o being OperSymbol of F1()
for ts being Element of Args o,(FreeMSA F2())
for x being FinSequence of Union the Sorts of F3() st x = (Flatten f1) * ts holds
(f1 . (the_result_sort_of o)) . ((Den o,(FreeMSA F2())) . ts) = H2(o,ts,x)
proof
let o be
OperSymbol of
F1();
:: thesis: for ts being Element of Args o,(FreeMSA F2())
for x being FinSequence of Union the Sorts of F3() st x = (Flatten f1) * ts holds
(f1 . (the_result_sort_of o)) . ((Den o,(FreeMSA F2())) . ts) = H2(o,ts,x)let ts be
Element of
Args o,
(FreeMSA F2());
:: thesis: for x being FinSequence of Union the Sorts of F3() st x = (Flatten f1) * ts holds
(f1 . (the_result_sort_of o)) . ((Den o,(FreeMSA F2())) . ts) = H2(o,ts,x)let x be
FinSequence of
Union the
Sorts of
F3();
:: thesis: ( x = (Flatten f1) * ts implies (f1 . (the_result_sort_of o)) . ((Den o,(FreeMSA F2())) . ts) = H2(o,ts,x) )
A17:
(Flatten f1) * ts = F4()
# ts
by A5, Th5;
assume A18:
x = (Flatten f1) * ts
;
:: thesis: (f1 . (the_result_sort_of o)) . ((Den o,(FreeMSA F2())) . ts) = H2(o,ts,x)
then reconsider a =
x as
Element of
Args o,
F3()
by A17;
A19:
[o,a] in R
by A12;
thus (f1 . (the_result_sort_of o)) . ((Den o,(FreeMSA F2())) . ts) =
(Den o,F3()) . a
by A1, A17, A18, MSUALG_3:def 9
.=
H . [o,x]
by A15, A19
.=
H /. [o,x]
by A19, CAT_3:def 1
;
:: thesis: verum
end;
A20:
for s being SortSymbol of F1()
for y being set st y in FreeGen s,F2() holds
(f1 . s) . y = H1(y)
A24:
for o being OperSymbol of F1()
for ts being Element of Args o,(FreeMSA F2())
for x being FinSequence of Union the Sorts of F3() st x = (Flatten f2) * ts holds
(f2 . (the_result_sort_of o)) . ((Den o,(FreeMSA F2())) . ts) = H2(o,ts,x)
proof
let o be
OperSymbol of
F1();
:: thesis: for ts being Element of Args o,(FreeMSA F2())
for x being FinSequence of Union the Sorts of F3() st x = (Flatten f2) * ts holds
(f2 . (the_result_sort_of o)) . ((Den o,(FreeMSA F2())) . ts) = H2(o,ts,x)let ts be
Element of
Args o,
(FreeMSA F2());
:: thesis: for x being FinSequence of Union the Sorts of F3() st x = (Flatten f2) * ts holds
(f2 . (the_result_sort_of o)) . ((Den o,(FreeMSA F2())) . ts) = H2(o,ts,x)let x be
FinSequence of
Union the
Sorts of
F3();
:: thesis: ( x = (Flatten f2) * ts implies (f2 . (the_result_sort_of o)) . ((Den o,(FreeMSA F2())) . ts) = H2(o,ts,x) )
A25:
(Flatten f2) * ts = F5()
# ts
by A5, Th5;
assume A26:
x = (Flatten f2) * ts
;
:: thesis: (f2 . (the_result_sort_of o)) . ((Den o,(FreeMSA F2())) . ts) = H2(o,ts,x)
then reconsider a =
x as
Element of
Args o,
F3()
by A25;
A27:
[o,a] in R
by A12;
thus (f2 . (the_result_sort_of o)) . ((Den o,(FreeMSA F2())) . ts) =
(Den o,F3()) . a
by A3, A25, A26, MSUALG_3:def 9
.=
H . [o,x]
by A15, A27
.=
H /. [o,x]
by A27, CAT_3:def 1
;
:: thesis: verum
end;
A28:
for s being SortSymbol of F1()
for y being set st y in FreeGen s,F2() holds
(f2 . s) . y = H1(y)
f1 = f2
from MSAFREE1:sch 2(A16, A20, A24, A28);
hence
F4() = F5()
; :: thesis: verum