deffunc H1( set , set , set ) -> compositional ManySortedFunction of [:(Funcs ($2,$3)),(Funcs ($1,$2)):] = FuncComp ((Funcs ($1,$2)),(Funcs ($2,$3)));
consider M being ManySortedSet of [:A,A:] such that
A1:
for i, j being set st i in A & j in A holds
M . (i,j) = Funcs (i,j)
from ALTCAT_1:sch 1();
consider c being ManySortedSet of [:A,A,A:] such that
A2:
for i, j, k being set st i in A & j in A & k in A holds
c . (i,j,k) = H1(i,j,k)
from ALTCAT_1:sch 3();
c is Function-yielding
proof
let i be
object ;
FUNCOP_1:def 6 ( not i in proj1 c or c . i is set )
assume
i in dom c
;
c . i is set
then
i in [:A,A,A:]
;
then consider x1,
x2,
x3 being
object such that A3:
(
x1 in A &
x2 in A &
x3 in A )
and A4:
i = [x1,x2,x3]
by MCART_1:68;
reconsider x1 =
x1,
x2 =
x2,
x3 =
x3 as
set by TARSKI:1;
c . i =
c . (
x1,
x2,
x3)
by A4, MULTOP_1:def 1
.=
FuncComp (
(Funcs (x1,x2)),
(Funcs (x2,x3)))
by A2, A3
;
hence
c . i is
set
;
verum
end;
then reconsider c = c as ManySortedFunction of [:A,A,A:] ;
now for i being object st i in [:A,A,A:] holds
c . i is Function of ({|M,M|} . i),({|M|} . i)let i be
object ;
( i in [:A,A,A:] implies c . i is Function of ({|M,M|} . i),({|M|} . i) )reconsider ci =
c . i as
Function ;
assume
i in [:A,A,A:]
;
c . i is Function of ({|M,M|} . i),({|M|} . i)then consider x1,
x2,
x3 being
object such that A5:
x1 in A
and A6:
x2 in A
and A7:
x3 in A
and A8:
i = [x1,x2,x3]
by MCART_1:68;
A9:
{|M|} . i =
{|M|} . (
x1,
x2,
x3)
by A8, MULTOP_1:def 1
.=
M . (
x1,
x3)
by A5, A6, A7, Def3
;
reconsider x1 =
x1,
x2 =
x2,
x3 =
x3 as
set by TARSKI:1;
A10:
c . i =
c . (
x1,
x2,
x3)
by A8, MULTOP_1:def 1
.=
FuncComp (
(Funcs (x1,x2)),
(Funcs (x2,x3)))
by A2, A5, A6, A7
;
(
M . (
x1,
x2)
= Funcs (
x1,
x2) &
M . (
x2,
x3)
= Funcs (
x2,
x3) )
by A1, A5, A6, A7;
then A11:
[:(Funcs (x2,x3)),(Funcs (x1,x2)):] =
{|M,M|} . (
x1,
x2,
x3)
by A5, A6, A7, Def4
.=
{|M,M|} . i
by A8, MULTOP_1:def 1
;
M . (
x1,
x3)
= Funcs (
x1,
x3)
by A1, A5, A7;
then A12:
rng ci c= {|M|} . i
by A10, A9, Th6;
dom ci = [:(Funcs (x2,x3)),(Funcs (x1,x2)):]
by A10, PARTFUN1:def 2;
hence
c . i is
Function of
({|M,M|} . i),
({|M|} . i)
by A11, A12, FUNCT_2:2;
verum end;
then reconsider c = c as BinComp of M by PBOOLE:def 15;
set C = AltCatStr(# A,M,c #);
AltCatStr(# A,M,c #) is pseudo-functional
proof
let o1,
o2,
o3 be
Object of
AltCatStr(#
A,
M,
c #);
ALTCAT_1:def 13 the Comp of AltCatStr(# A,M,c #) . (o1,o2,o3) = (FuncComp ((Funcs (o1,o2)),(Funcs (o2,o3)))) | [:<^o2,o3^>,<^o1,o2^>:]
(
<^o1,o2^> = Funcs (
o1,
o2) &
<^o2,o3^> = Funcs (
o2,
o3) )
by A1;
then A13:
dom (FuncComp ((Funcs (o1,o2)),(Funcs (o2,o3)))) = [:<^o2,o3^>,<^o1,o2^>:]
by PARTFUN1:def 2;
thus the
Comp of
AltCatStr(#
A,
M,
c #)
. (
o1,
o2,
o3) =
FuncComp (
(Funcs (o1,o2)),
(Funcs (o2,o3)))
by A2
.=
(FuncComp ((Funcs (o1,o2)),(Funcs (o2,o3)))) | [:<^o2,o3^>,<^o1,o2^>:]
by A13
;
verum
end;
then reconsider C = AltCatStr(# A,M,c #) as non empty strict pseudo-functional AltCatStr ;
take
C
; ( the carrier of C = A & ( for a1, a2 being Object of C holds <^a1,a2^> = Funcs (a1,a2) ) )
thus
the carrier of C = A
; for a1, a2 being Object of C holds <^a1,a2^> = Funcs (a1,a2)
let a1, a2 be Object of C; <^a1,a2^> = Funcs (a1,a2)
thus
<^a1,a2^> = Funcs (a1,a2)
by A1; verum