consider M being ManySortedSet of 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();
deffunc H1( set , set , set ) -> compositional ManySortedFunction of = FuncComp (Funcs $1,$2),(Funcs $2,$3);
consider c being ManySortedSet of 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
set ;
:: according to FUNCOP_1:def 6 :: thesis: ( not i in dom c or c . i is set )
assume
i in dom c
;
:: thesis: c . i is set
then
i in [:A,A,A:]
by PARTFUN1:def 4;
then consider x1,
x2,
x3 being
set such that A3:
(
x1 in A &
x2 in A &
x3 in A )
and A4:
i = [x1,x2,x3]
by MCART_1:72;
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
;
:: thesis: verum
end;
then reconsider c = c as ManySortedFunction of ;
now let i be
set ;
:: thesis: ( i in [:A,A,A:] implies c . i is Function of ({|M,M|} . i),({|M|} . i) )assume
i in [:A,A,A:]
;
:: thesis: c . i is Function of ({|M,M|} . i),({|M|} . i)then consider x1,
x2,
x3 being
set such that A5:
(
x1 in A &
x2 in A &
x3 in A )
and A6:
i = [x1,x2,x3]
by MCART_1:72;
A7:
M . x1,
x2 = Funcs x1,
x2
by A1, A5;
A8:
M . x2,
x3 = Funcs x2,
x3
by A1, A5;
A9:
M . x1,
x3 = Funcs x1,
x3
by A1, A5;
A10:
c . i =
c . x1,
x2,
x3
by A6, MULTOP_1:def 1
.=
FuncComp (Funcs x1,x2),
(Funcs x2,x3)
by A2, A5
;
reconsider ci =
c . i as
Function ;
A11:
dom ci = [:(Funcs x2,x3),(Funcs x1,x2):]
by A10, PARTFUN1:def 4;
A12:
[:(Funcs x2,x3),(Funcs x1,x2):] =
{|M,M|} . x1,
x2,
x3
by A5, A7, A8, Def6
.=
{|M,M|} . i
by A6, MULTOP_1:def 1
;
A13:
{|M|} . i =
{|M|} . x1,
x2,
x3
by A6, MULTOP_1:def 1
.=
M . x1,
x3
by A5, Def5
;
then A14:
rng ci c= {|M|} . i
by A9, A10, Th14;
now assume
{|M,M|} . i <> {}
;
:: thesis: {|M|} . i <> {} then consider j being
set such that A15:
j in [:(Funcs x2,x3),(Funcs x1,x2):]
by A12, XBOOLE_0:def 1;
consider j1,
j2 being
set such that A16:
j1 in Funcs x2,
x3
and A17:
j2 in Funcs x1,
x2
and
j = [j1,j2]
by A15, ZFMISC_1:103;
reconsider j1 =
j1 as
Function of
x2,
x3 by A16, FUNCT_2:121;
reconsider j2 =
j2 as
Function of
x1,
x2 by A17, FUNCT_2:121;
j1 * j2 in Funcs x1,
x3
by A16, A17, Th4;
hence
{|M|} . i <> {}
by A1, A5, A13;
:: thesis: verum end; hence
c . i is
Function of
({|M,M|} . i),
({|M|} . i)
by A11, A12, A14, FUNCT_2:def 1, RELSET_1:11;
:: thesis: verum end;
then reconsider c = c as BinComp of M by PBOOLE:def 18;
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 #);
:: according to ALTCAT_1:def 15 :: thesis: the Comp of AltCatStr(# A,M,c #) . o1,o2,o3 = (FuncComp (Funcs o1,o2),(Funcs o2,o3)) | [:<^o2,o3^>,<^o1,o2^>:]
A18:
<^o1,o2^> = Funcs o1,
o2
by A1;
<^o2,o3^> = Funcs o2,
o3
by A1;
then A19:
dom (FuncComp (Funcs o1,o2),(Funcs o2,o3)) = [:<^o2,o3^>,<^o1,o2^>:]
by A18, PARTFUN1:def 4;
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 A19, RELAT_1:97
;
:: thesis: verum
end;
then reconsider C = AltCatStr(# A,M,c #) as non empty strict pseudo-functional AltCatStr ;
take
C
; :: thesis: ( the carrier of C = A & ( for a1, a2 being object of C holds <^a1,a2^> = Funcs a1,a2 ) )
thus
the carrier of C = A
; :: thesis: for a1, a2 being object of C holds <^a1,a2^> = Funcs a1,a2
let a1, a2 be object of C; :: thesis: <^a1,a2^> = Funcs a1,a2
thus
<^a1,a2^> = Funcs a1,a2
by A1; :: thesis: verum