deffunc H1( set , set , set ) -> set = FuncComp (F2($1,$2),F2($2,$3));
consider M being ManySortedSet of [:F1(),F1():] such that
A2:
for i, j being Element of F1() holds M . (i,j) = F2(i,j)
from ALTCAT_1:sch 2();
consider c being ManySortedSet of [:F1(),F1(),F1():] such that
A3:
for i, j, k being Element of F1() holds c . (i,j,k) = H1(i,j,k)
from ALTCAT_1:sch 4();
c is Function-yielding
proof
let i be
object ;
FUNCOP_1:def 6 ( not i in dom c or c . i is set )
assume
i in dom c
;
c . i is set
then
i in [:F1(),F1(),F1():]
;
then consider x1,
x2,
x3 being
object such that A4:
(
x1 in F1() &
x2 in F1() &
x3 in F1() )
and A5:
i = [x1,x2,x3]
by MCART_1:68;
c . i =
c . (
x1,
x2,
x3)
by A5, MULTOP_1:def 1
.=
FuncComp (
F2(
x1,
x2),
F2(
x2,
x3))
by A3, A4
;
hence
c . i is
set
;
verum
end;
then reconsider c = c as ManySortedFunction of [:F1(),F1(),F1():] ;
now for i being object st i in [:F1(),F1(),F1():] holds
c . i is Function of ({|M,M|} . i),({|M|} . i)let i be
object ;
( i in [:F1(),F1(),F1():] implies c . i is Function of ({|M,M|} . i),({|M|} . i) )assume
i in [:F1(),F1(),F1():]
;
c . i is Function of ({|M,M|} . i),({|M|} . i)then consider x1,
x2,
x3 being
object such that A6:
x1 in F1()
and A7:
x2 in F1()
and A8:
x3 in F1()
and A9:
i = [x1,x2,x3]
by MCART_1:68;
M . (
x1,
x2)
= F2(
x1,
x2)
by A2, A6, A7;
then A10:
[:F2(x2,x3),F2(x1,x2):] =
[:(M . (x2,x3)),(M . (x1,x2)):]
by A2, A7, A8
.=
{|M,M|} . (
x1,
x2,
x3)
by A6, A7, A8, ALTCAT_1:def 4
.=
{|M,M|} . i
by A9, MULTOP_1:def 1
;
A11:
{|M|} . i =
{|M|} . (
x1,
x2,
x3)
by A9, MULTOP_1:def 1
.=
M . (
x1,
x3)
by A6, A7, A8, ALTCAT_1:def 3
;
A12:
now ( {|M,M|} . i <> {} implies {|M|} . i <> {} )assume
{|M,M|} . i <> {}
;
{|M|} . i <> {} then consider j being
object such that A13:
j in [:F2(x2,x3),F2(x1,x2):]
by A10, XBOOLE_0:def 1;
consider j1,
j2 being
object such that A14:
j1 in F2(
x2,
x3)
and A15:
j2 in F2(
x1,
x2)
and
j = [j1,j2]
by A13, ZFMISC_1:84;
reconsider j2 =
j2 as
Function by A15;
reconsider j1 =
j1 as
Function by A14;
j1 * j2 in F2(
x1,
x3)
by A1, A6, A7, A8, A14, A15;
hence
{|M|} . i <> {}
by A2, A6, A8, A11;
verum end; A16:
c . i =
c . (
x1,
x2,
x3)
by A9, MULTOP_1:def 1
.=
FuncComp (
F2(
x1,
x2),
F2(
x2,
x3))
by A3, A6, A7, A8
;
then reconsider ci =
c . i as
Function ;
A17:
dom ci = [:F2(x2,x3),F2(x1,x2):]
by A16, PARTFUN1:def 2;
rng (FuncComp (F2(x1,x2),F2(x2,x3))) c= F2(
x1,
x3)
proof
set F =
FuncComp (
F2(
x1,
x2),
F2(
x2,
x3));
let i be
object ;
TARSKI:def 3 ( not i in rng (FuncComp (F2(x1,x2),F2(x2,x3))) or i in F2(x1,x3) )
assume
i in rng (FuncComp (F2(x1,x2),F2(x2,x3)))
;
i in F2(x1,x3)
then consider j being
object such that A18:
j in dom (FuncComp (F2(x1,x2),F2(x2,x3)))
and A19:
i = (FuncComp (F2(x1,x2),F2(x2,x3))) . j
by FUNCT_1:def 3;
consider f,
g being
Function such that A20:
j = [g,f]
and A21:
(FuncComp (F2(x1,x2),F2(x2,x3))) . j = g * f
by A18, ALTCAT_1:def 9;
(
g in F2(
x2,
x3) &
f in F2(
x1,
x2) )
by A18, A20, ZFMISC_1:87;
hence
i in F2(
x1,
x3)
by A1, A6, A7, A8, A19, A21;
verum
end; then
rng ci c= {|M|} . i
by A2, A6, A8, A16, A11;
hence
c . i is
Function of
({|M,M|} . i),
({|M|} . i)
by A17, A10, A12, FUNCT_2:def 1, RELSET_1:4;
verum end;
then reconsider c = c as BinComp of M by PBOOLE:def 15;
set C = AltCatStr(# F1(),M,c #);
take
AltCatStr(# F1(),M,c #)
; ( the carrier of AltCatStr(# F1(),M,c #) = F1() & ( for i, j being Element of F1() holds
( the Arrows of AltCatStr(# F1(),M,c #) . (i,j) = F2(i,j) & ( for i, j, k being Element of F1() holds the Comp of AltCatStr(# F1(),M,c #) . (i,j,k) = FuncComp (F2(i,j),F2(j,k)) ) ) ) )
thus
the carrier of AltCatStr(# F1(),M,c #) = F1()
; for i, j being Element of F1() holds
( the Arrows of AltCatStr(# F1(),M,c #) . (i,j) = F2(i,j) & ( for i, j, k being Element of F1() holds the Comp of AltCatStr(# F1(),M,c #) . (i,j,k) = FuncComp (F2(i,j),F2(j,k)) ) )
let i, j be Element of F1(); ( the Arrows of AltCatStr(# F1(),M,c #) . (i,j) = F2(i,j) & ( for i, j, k being Element of F1() holds the Comp of AltCatStr(# F1(),M,c #) . (i,j,k) = FuncComp (F2(i,j),F2(j,k)) ) )
thus
the Arrows of AltCatStr(# F1(),M,c #) . (i,j) = F2(i,j)
by A2; for i, j, k being Element of F1() holds the Comp of AltCatStr(# F1(),M,c #) . (i,j,k) = FuncComp (F2(i,j),F2(j,k))
let i, j, k be Element of F1(); the Comp of AltCatStr(# F1(),M,c #) . (i,j,k) = FuncComp (F2(i,j),F2(j,k))
thus
the Comp of AltCatStr(# F1(),M,c #) . (i,j,k) = FuncComp (F2(i,j),F2(j,k))
by A3; verum