defpred S1[ set , set ] means for s being SortSymbol of F1() st $1 in FreeGen (s,F2()) holds
P1[s,$2,$1];
A5:
FreeMSA F2() = MSAlgebra(# (FreeSort F2()),(FreeOper F2()) #)
by MSAFREE:def 14;
then reconsider f1 = F4(), f2 = F5() as ManySortedFunction of FreeSort F2(), the Sorts of F3() ;
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 ;
( e in Union (FreeGen F2()) implies ex y being set st
( y in Union the Sorts of F3() & S1[e,y] ) )
A7:
dom the
Sorts of
F3()
= the
carrier of
F1()
by PARTFUN1:def 2;
assume
e in Union (FreeGen F2())
;
ex y being set st
( y in Union the Sorts of F3() & S1[e,y] )
then consider s being
set such that A8:
s in dom (FreeGen F2())
and A9:
e in (FreeGen F2()) . s
by CARD_5:2;
reconsider s =
s as
SortSymbol of
F1()
by A8, PARTFUN1:def 2;
A10:
e in FreeGen (
s,
F2())
by A9, MSAFREE:def 16;
take u =
(F4() . s) . e;
( u in Union the Sorts of F3() & S1[e,u] )
f1 . s is
Function of
((FreeSort F2()) . s),
( the Sorts of F3() . s)
;
then
u in the
Sorts of
F3()
. s
by A10, FUNCT_2:5;
hence
u in Union the
Sorts of
F3()
by A7, CARD_5:2;
S1[e,u]
let s9 be
SortSymbol of
F1();
( e in FreeGen (s9,F2()) implies P1[s9,u,e] )
assume A11:
e in FreeGen (
s9,
F2())
;
P1[s9,u,e]
then
((FreeSort F2()) . s9) /\ ((FreeSort F2()) . s) <> {}
by A10, XBOOLE_0:def 4;
then
(FreeSort F2()) . s9 meets (FreeSort F2()) . s
by XBOOLE_0:def 7;
then
s = s9
by MSAFREE:12;
hence
P1[
s9,
u,
e]
by A2, A11;
verum
end;
consider G being Function of (Union (FreeGen F2())),(Union the Sorts of F3()) such that
A12:
for e being set st e in Union (FreeGen F2()) holds
S1[e,G . e]
from FUNCT_2:sch 1(A6);
deffunc H1( set ) -> Element of Union the Sorts of F3() = G /. $1;
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;
consider R being set such that
A13:
R = { [o,a] where o is Element of the carrier' of F1(), a is Element of Args (o,F3()) : verum }
;
A14:
for s being SortSymbol of F1()
for y being set st y in FreeGen (s,F2()) holds
(f1 . s) . y = H1(y)
A18:
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 ;
( e in R implies ex y being set st
( y in Union the Sorts of F3() & S2[e,y] ) )
assume
e in R
;
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 A19:
e = [o,a]
by A13;
reconsider u =
(Den (o,F3())) . a as
set ;
take
u
;
( 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;
S2[e,u]
let o9 be
OperSymbol of
F1();
for a being Element of Args (o9,F3()) st e = [o9,a] holds
u = (Den (o9,F3())) . alet x9 be
Element of
Args (
o9,
F3());
( e = [o9,x9] implies u = (Den (o9,F3())) . x9 )
assume A20:
e = [o9,x9]
;
u = (Den (o9,F3())) . x9
then
o = o9
by A19, ZFMISC_1:27;
hence
u = (Den (o9,F3())) . x9
by A19, A20, ZFMISC_1:27;
verum
end;
consider H being Function of R,(Union the Sorts of F3()) such that
A21:
for e being set st e in R holds
S2[e,H . e]
from FUNCT_2:sch 1(A18);
A22:
for s being SortSymbol of F1()
for y being set st y in FreeGen (s,F2()) holds
(f2 . s) . y = H1(y)
deffunc H2( set , set , set ) -> Element of Union the Sorts of F3() = H /. [$1,$3];
A26:
for o being OperSymbol of F1()
for ts being Element of Args (o,(FreeMSA F2()))
for x being Element 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();
for ts being Element of Args (o,(FreeMSA F2()))
for x being Element 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()));
for x being Element 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
Element of
(Union the Sorts of F3()) * ;
( x = (Flatten f2) * ts implies (f2 . (the_result_sort_of o)) . ((Den (o,(FreeMSA F2()))) . ts) = H2(o,ts,x) )
assume A27:
x = (Flatten f2) * ts
;
(f2 . (the_result_sort_of o)) . ((Den (o,(FreeMSA F2()))) . ts) = H2(o,ts,x)
A28:
(Flatten f2) * ts = F5()
# ts
by A5, Th5;
then reconsider a =
x as
Element of
Args (
o,
F3())
by A27;
A29:
[o,a] in R
by A13;
thus (f2 . (the_result_sort_of o)) . ((Den (o,(FreeMSA F2()))) . ts) =
(Den (o,F3())) . a
by A3, A28, A27, MSUALG_3:def 7
.=
H . [o,x]
by A21, A29
.=
H /. [o,x]
by A29, FUNCT_2:def 13
;
verum
end;
A30:
for o being OperSymbol of F1()
for ts being Element of Args (o,(FreeMSA F2()))
for x being Element 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();
for ts being Element of Args (o,(FreeMSA F2()))
for x being Element 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()));
for x being Element 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
Element of
(Union the Sorts of F3()) * ;
( x = (Flatten f1) * ts implies (f1 . (the_result_sort_of o)) . ((Den (o,(FreeMSA F2()))) . ts) = H2(o,ts,x) )
assume A31:
x = (Flatten f1) * ts
;
(f1 . (the_result_sort_of o)) . ((Den (o,(FreeMSA F2()))) . ts) = H2(o,ts,x)
A32:
(Flatten f1) * ts = F4()
# ts
by A5, Th5;
then reconsider a =
x as
Element of
Args (
o,
F3())
by A31;
A33:
[o,a] in R
by A13;
thus (f1 . (the_result_sort_of o)) . ((Den (o,(FreeMSA F2()))) . ts) =
(Den (o,F3())) . a
by A1, A32, A31, MSUALG_3:def 7
.=
H . [o,x]
by A21, A33
.=
H /. [o,x]
by A33, FUNCT_2:def 13
;
verum
end;
f1 = f2
from MSAFREE1:sch 2(A30, A14, A26, A22);
hence
F4() = F5()
; verum