:: ALTCAT_1 semantic presentation
theorem :: ALTCAT_1:1
canceled;
theorem E1: :: ALTCAT_1:2
theorem E2: :: ALTCAT_1:3
theorem E3: :: ALTCAT_1:4
theorem E4: :: ALTCAT_1:5
proof
let c
1, c
2, c
3 be
set ;
assume that
E5:
Funcs c
1,c
2 <> {}
and
E6:
Funcs c
2,c
3 <> {}
;
consider c
4 being
set such that
E7:
c
4 in Funcs c
1,c
2
by E5, XBOOLE_0:def 1;
consider c
5 being
set such that
E8:
c
5 in Funcs c
2,c
3
by E6, XBOOLE_0:def 1;
reconsider c
6 = c
4 as
Function of c
1,c
2 by E7, FUNCT_2:121;
reconsider c
7 = c
5 as
Function of c
2,c
3 by E8, FUNCT_2:121;
c
6 * c
7 in Funcs c
1,c
3
by E7, E8, E3;
hence
Funcs c
1,c
3 <> {}
;
end;
theorem :: ALTCAT_1:6
canceled;
theorem :: ALTCAT_1:7
proof
let c
1, c
2 be
set ;
let c
3 be
ManySortedSet of
[:c2,c1:];
let c
4 be
Subset of c
1;
let c
5 be
Subset of c
2;
let c
6, c
7 be
set ;
assume
( c
6 in c
4 & c
7 in c
5 )
;
then E5:
[c7,c6] in [:c5,c4:]
by ZFMISC_1:106;
thus c
3 . c
7,c
6 =
c
3 . [c7,c6]
by BINOP_1:def 1
.=
(c3 | [:c5,c4:]) . [c7,c6]
by E5, FUNCT_1:72
.=
(c3 | [:c5,c4:]) . c
7,c
6
by BINOP_1:def 1
;
end;
scheme :: ALTCAT_1:sch 1
s1{ F
1()
-> set , F
2()
-> set , F
3(
set ,
set )
-> set } :
ex b
1 being
ManySortedSet of
[:F1(),F2():] st
for b
2, b
3 being
set holds
( ( b
2 in F
1() & b
3 in F
2() ) implies ( b
1 . b
2,b
3 = F
3(b
2,b
3) ) )
proof
deffunc H
1(
set )
-> set = F
3(
(a1 `1 ),
(a1 `2 ));
consider c
1 being
Function such that
E5:
dom c
1 = [:F1(),F2():]
and
E6:
for b
1 being
set holds
( b
1 in [:F1(),F2():] implies c
1 . b
1 = H
1(b
1) )
from FUNCT_1:sch 3();
reconsider c
2 = c
1 as
ManySortedSet of
[:F1(),F2():] by E5, PBOOLE:def 3;
take
c
2
;
let c
3, c
4 be
set ;
assume
( c
3 in F
1() & c
4 in F
2() )
;
then E7:
[c3,c4] in [:F1(),F2():]
by ZFMISC_1:106;
E8:
(
[c3,c4] `1 = c
3 &
[c3,c4] `2 = c
4 )
by MCART_1:7;
thus c
2 . c
3,c
4 =
c
2 . [c3,c4]
by BINOP_1:def 1
.=
F
3(c
3,c
4)
by E6, E7, E8
;
end;
scheme :: ALTCAT_1:sch 3
s3{ F
1()
-> set , F
2()
-> set , F
3()
-> set , F
4(
set ,
set ,
set )
-> set } :
ex b
1 being
ManySortedSet of
[:F1(),F2(),F3():] st
for b
2, b
3, b
4 being
set holds
( ( b
2 in F
1() & b
3 in F
2() & b
4 in F
3() ) implies ( b
1 . b
2,b
3,b
4 = F
4(b
2,b
3,b
4) ) )
proof
deffunc H
1(
set )
-> set = F
4(
((a1 `1 ) `1 ),
((a1 `1 ) `2 ),
(a1 `2 ));
consider c
1 being
Function such that
E5:
dom c
1 = [:F1(),F2(),F3():]
and
E6:
for b
1 being
set holds
( b
1 in [:F1(),F2(),F3():] implies c
1 . b
1 = H
1(b
1) )
from FUNCT_1:sch 3();
reconsider c
2 = c
1 as
ManySortedSet of
[:F1(),F2(),F3():] by E5, PBOOLE:def 3;
take
c
2
;
let c
3, c
4, c
5 be
set ;
assume
( c
3 in F
1() & c
4 in F
2() & c
5 in F
3() )
;
then E7:
[c3,c4,c5] in [:F1(),F2(),F3():]
by MCART_1:73;
(
[c3,c4] `1 = c
3 &
[c3,c4] `2 = c
4 )
by MCART_1:7;
then E8:
(
([[c3,c4],c5] `1 ) `1 = c
3 &
([[c3,c4],c5] `1 ) `2 = c
4 &
[[c3,c4],c5] `2 = c
5 )
by MCART_1:7;
E9:
[c3,c4,c5] = [[c3,c4],c5]
by MCART_1:def 3;
thus c
2 . c
3,c
4,c
5 =
c
2 . [c3,c4,c5]
by MULTOP_1:def 1
.=
F
4(c
3,c
4,c
5)
by E6, E7, E8, E9
;
end;
scheme :: ALTCAT_1:sch 4
s4{ F
1()
-> non
empty set , F
2()
-> non
empty set , F
3()
-> non
empty set , F
4(
set ,
set ,
set )
-> set } :
provided
proof
consider c
1 being
ManySortedSet of
[:F1(),F2(),F3():] such that
E5:
for b
1, b
2, b
3 being
set holds
( ( b
1 in F
1() & b
2 in F
2() & b
3 in F
3() ) implies ( c
1 . b
1,b
2,b
3 = F
4(b
1,b
2,b
3) ) )
from ALTCAT_1:sch 3();
take
c
1
;
thus
for b
1 being
Element of F
1()
for b
2 being
Element of F
2()
for b
3 being
Element of F
3() holds c
1 . b
1,b
2,b
3 = F
4(b
1,b
2,b
3)
by E5;
end;
theorem E5: :: ALTCAT_1:8
for b
1, b
2 being
set for b
3, b
4 being
ManySortedSet of
[:b1,b2:] holds
( for b
5, b
6 being
set holds
( ( b
5 in b
1 & b
6 in b
2 ) implies ( b
3 . b
5,b
6 = b
4 . b
5,b
6 ) ) implies b
4 = b
3 )
theorem E6: :: ALTCAT_1:9
proof
let c
1, c
2 be non
empty set ;
let c
3, c
4 be
ManySortedSet of
[:c1,c2:];
assume
for b
1 being
Element of c
1for b
2 being
Element of c
2 holds c
3 . b
1,b
2 = c
4 . b
1,b
2
;
then
for b
1, b
2 being
set holds
( ( b
1 in c
1 & b
2 in c
2 ) implies ( c
3 . b
1,b
2 = c
4 . b
1,b
2 ) )
;
hence
c
4 = c
3
by E5;
end;
theorem E7: :: ALTCAT_1:10
for b
1 being
set for b
2, b
3 being
ManySortedSet of
[:b1,b1,b1:] holds
( for b
4, b
5, b
6 being
set holds
( ( b
4 in b
1 & b
5 in b
1 & b
6 in b
1 ) implies ( b
2 . b
4,b
5,b
6 = b
3 . b
4,b
5,b
6 ) ) implies b
3 = b
2 )
proof
let c
1 be
set ;
let c
2, c
3 be
ManySortedSet of
[:c1,c1,c1:];
assume E8:
for b
1, b
2, b
3 being
set holds
( ( b
1 in c
1 & b
2 in c
1 & b
3 in c
1 ) implies ( c
2 . b
1,b
2,b
3 = c
3 . b
1,b
2,b
3 ) )
;
E9:
(
dom c
3 = [:c1,c1,c1:] &
dom c
2 = [:c1,c1,c1:] )
by PBOOLE:def 3;
now
let c
4 be
set ;
assume E10:
c
4 in [:c1,c1,c1:]
;
then reconsider c
5 = c
1 as non
empty set by MCART_1:35;
consider c
6, c
7, c
8 being
Element of c
5 such that
E11:
c
4 = [c6,c7,c8]
by E10, DOMAIN_1:15;
thus c
3 . c
4 =
c
3 . c
6,c
7,c
8
by E11, MULTOP_1:def 1
.=
c
2 . c
6,c
7,c
8
by E8
.=
c
2 . c
4
by E11, MULTOP_1:def 1
;
end;
hence
c
3 = c
2
by E9, FUNCT_1:9;
end;
theorem E8: :: ALTCAT_1:11
proof
let c
1, c
2, c
3 be
set ;
E9:
{[c1,c2]} = [:{c1},{c2}:]
by ZFMISC_1:35;
(
dom ([c1,c2] .--> c3) = {[c1,c2]} &
rng ([c1,c2] .--> c3) = {c3} )
by CQC_LANG:5;
then
[c1,c2] .--> c
3 is
Function of
[:{c1},{c2}:],
{c3}
by E9, FUNCT_2:def 1, RELSET_1:11;
hence
c
1,c
2 :-> c
3 = [c1,c2] .--> c
3
by FUNCT_2:def 5;
end;
theorem E9: :: ALTCAT_1:12
for b
1, b
2, b
3 being
set holds
(b1,b2 :-> b3) . b
1,b
2 = b
3
:: deftheorem ALTCAT_1:def 1 :
canceled;
:: deftheorem defines <^ ALTCAT_1:def 2 :
:: deftheorem ALTCAT_1:def 3 :
canceled;
:: deftheorem E10 defines transitive ALTCAT_1:def 4 :
definition
let c
1 be
set ;
let c
2 be
ManySortedSet of
[:c1,c1:];
func {|a2|} -> ManySortedSet of
[:a1,a1,a1:] means :
E11:
:: ALTCAT_1:def 5
for b
1, b
2, b
3 being
set holds
( ( b
1 in a
1 & b
2 in a
1 & b
3 in a
1 ) implies ( a
3 . b
1,b
2,b
3 = a
2 . b
1,b
3 ) );
existence
ex b1 being ManySortedSet of [:c1,c1,c1:] st
for b2, b3, b4 being set holds
( ( b2 in c1 & b3 in c1 & b4 in c1 ) implies ( b1 . b2,b3,b4 = c2 . b2,b4 ) )
proof
deffunc H
1(
set ,
set ,
set )
-> set = c
2 . a
1,a
3;
ex b
1 being
ManySortedSet of
[:c1,c1,c1:] st
for b
2, b
3, b
4 being
set holds
( ( b
2 in c
1 & b
3 in c
1 & b
4 in c
1 ) implies ( b
1 . b
2,b
3,b
4 = H
1(b
2,b
3,b
4) ) )
from ALTCAT_1:sch 3();
hence
ex b
1 being
ManySortedSet of
[:c1,c1,c1:] st
for b
2, b
3, b
4 being
set holds
( ( b
2 in c
1 & b
3 in c
1 & b
4 in c
1 ) implies ( b
1 . b
2,b
3,b
4 = c
2 . b
2,b
4 ) )
;
end;
uniqueness
for b1, b2 being ManySortedSet of [:c1,c1,c1:] holds
( ( for b3, b4, b5 being set holds
( ( b3 in c1 & b4 in c1 & b5 in c1 ) implies ( b1 . b3,b4,b5 = c2 . b3,b5 ) ) & for b3, b4, b5 being set holds
( ( b3 in c1 & b4 in c1 & b5 in c1 ) implies ( b2 . b3,b4,b5 = c2 . b3,b5 ) ) ) implies ( b1 = b2 ) )
proof
let c
3, c
4 be
ManySortedSet of
[:c1,c1,c1:];
assume that
E11:
for b
1, b
2, b
3 being
set holds
( ( b
1 in c
1 & b
2 in c
1 & b
3 in c
1 ) implies ( c
3 . b
1,b
2,b
3 = c
2 . b
1,b
3 ) )
and
E12:
for b
1, b
2, b
3 being
set holds
( ( b
1 in c
1 & b
2 in c
1 & b
3 in c
1 ) implies ( c
4 . b
1,b
2,b
3 = c
2 . b
1,b
3 ) )
;
now
let c
5, c
6, c
7 be
set ;
assume E13:
( c
5 in c
1 & c
6 in c
1 & c
7 in c
1 )
;
hence c
3 . c
5,c
6,c
7 =
c
2 . c
5,c
7
by E11
.=
c
4 . c
5,c
6,c
7
by E12, E13
;
end;
hence
c
3 = c
4
by E7;
end;
let c
3 be
ManySortedSet of
[:c1,c1:];
func {|a2,a3|} -> ManySortedSet of
[:a1,a1,a1:] means :
E12:
:: ALTCAT_1:def 6
for b
1, b
2, b
3 being
set holds
( ( b
1 in a
1 & b
2 in a
1 & b
3 in a
1 ) implies ( a
4 . b
1,b
2,b
3 = [:(a3 . b2,b3),(a2 . b1,b2):] ) );
existence
ex b1 being ManySortedSet of [:c1,c1,c1:] st
for b2, b3, b4 being set holds
( ( b2 in c1 & b3 in c1 & b4 in c1 ) implies ( b1 . b2,b3,b4 = [:(c3 . b3,b4),(c2 . b2,b3):] ) )
proof
deffunc H
1(
set ,
set ,
set )
-> set =
[:(c3 . a2,a3),(c2 . a1,a2):];
ex b
1 being
ManySortedSet of
[:c1,c1,c1:] st
for b
2, b
3, b
4 being
set holds
( ( b
2 in c
1 & b
3 in c
1 & b
4 in c
1 ) implies ( b
1 . b
2,b
3,b
4 = H
1(b
2,b
3,b
4) ) )
from ALTCAT_1:sch 3();
hence
ex b
1 being
ManySortedSet of
[:c1,c1,c1:] st
for b
2, b
3, b
4 being
set holds
( ( b
2 in c
1 & b
3 in c
1 & b
4 in c
1 ) implies ( b
1 . b
2,b
3,b
4 = [:(c3 . b3,b4),(c2 . b2,b3):] ) )
;
end;
uniqueness
for b1, b2 being ManySortedSet of [:c1,c1,c1:] holds
( ( for b3, b4, b5 being set holds
( ( b3 in c1 & b4 in c1 & b5 in c1 ) implies ( b1 . b3,b4,b5 = [:(c3 . b4,b5),(c2 . b3,b4):] ) ) & for b3, b4, b5 being set holds
( ( b3 in c1 & b4 in c1 & b5 in c1 ) implies ( b2 . b3,b4,b5 = [:(c3 . b4,b5),(c2 . b3,b4):] ) ) ) implies ( b1 = b2 ) )
proof
let c
4, c
5 be
ManySortedSet of
[:c1,c1,c1:];
assume that
E11:
for b
1, b
2, b
3 being
set holds
( ( b
1 in c
1 & b
2 in c
1 & b
3 in c
1 ) implies ( c
4 . b
1,b
2,b
3 = [:(c3 . b2,b3),(c2 . b1,b2):] ) )
and
E12:
for b
1, b
2, b
3 being
set holds
( ( b
1 in c
1 & b
2 in c
1 & b
3 in c
1 ) implies ( c
5 . b
1,b
2,b
3 = [:(c3 . b2,b3),(c2 . b1,b2):] ) )
;
now
let c
6, c
7, c
8 be
set ;
assume E13:
( c
6 in c
1 & c
7 in c
1 & c
8 in c
1 )
;
hence c
4 . c
6,c
7,c
8 =
[:(c3 . c7,c8),(c2 . c6,c7):]
by E11
.=
c
5 . c
6,c
7,c
8
by E12, E13
;
end;
hence
c
4 = c
5
by E7;
end;
end;
:: deftheorem E11 defines {| ALTCAT_1:def 5 :
:: deftheorem E12 defines {| ALTCAT_1:def 6 :
for b
1 being
set for b
2, b
3 being
ManySortedSet of
[:b1,b1:]for b
4 being
ManySortedSet of
[:b1,b1,b1:] holds
( b
4 = {|b2,b3|} iff for b
5, b
6, b
7 being
set holds
( ( b
5 in b
1 & b
6 in b
1 & b
7 in b
1 ) implies ( b
4 . b
5,b
6,b
7 = [:(b3 . b6,b7),(b2 . b5,b6):] ) ) );
definition
let c
1 be non
empty set ;
let c
2 be
ManySortedSet of
[:c1,c1:];
let c
3 be
BinComp of c
2;
let c
4, c
5, c
6 be
Element of c
1;
redefine func . as a
3 . a
4,a
5,a
6 -> Function of
[:(a2 . a5,a6),(a2 . a4,a5):],a
2 . a
4,a
6;
coherence
c3 . c4,c5,c6 is Function of [:(c2 . c5,c6),(c2 . c4,c5):],c2 . c4,c6
proof
E13:
c
3 . [c4,c5,c6] = c
3 . c
4,c
5,c
6
by MULTOP_1:def 1;
E14:
{|c2,c2|} . [c4,c5,c6] =
{|c2,c2|} . c
4,c
5,c
6
by MULTOP_1:def 1
.=
[:(c2 . c5,c6),(c2 . c4,c5):]
by E12
;
{|c2|} . [c4,c5,c6] =
{|c2|} . c
4,c
5,c
6
by MULTOP_1:def 1
.=
c
2 . c
4,c
6
by E11
;
hence
c
3 . c
4,c
5,c
6 is
Function of
[:(c2 . c5,c6),(c2 . c4,c5):],c
2 . c
4,c
6
by E13, E14, PBOOLE:def 18;
end;
end;
definition
let c
1 be non
empty set ;
let c
2 be
ManySortedSet of
[:c1,c1:];
let c
3 be
BinComp of c
2;
attr a
3 is
associative means :
E13:
:: ALTCAT_1:def 7
for b
1, b
2, b
3, b
4 being
Element of a
1for b
5, b
6, b
7 being
set holds
( ( b
5 in a
2 . b
1,b
2 & b
6 in a
2 . b
2,b
3 & b
7 in a
2 . b
3,b
4 ) implies (
(a3 . b1,b3,b4) . b
7,
((a3 . b1,b2,b3) . b6,b5) = (a3 . b1,b2,b4) . ((a3 . b2,b3,b4) . b7,b6),b
5 ) );
attr a
3 is
with_right_units means :
E14:
:: ALTCAT_1:def 8
for b
1 being
Element of a
1 holds
ex b
2 being
set st
( b
2 in a
2 . b
1,b
1 & for b
3 being
Element of a
1for b
4 being
set holds
( b
4 in a
2 . b
1,b
3 implies
(a3 . b1,b1,b3) . b
4,b
2 = b
4 ) );
attr a
3 is
with_left_units means :
E15:
:: ALTCAT_1:def 9
for b
1 being
Element of a
1 holds
ex b
2 being
set st
( b
2 in a
2 . b
1,b
1 & for b
3 being
Element of a
1for b
4 being
set holds
( b
4 in a
2 . b
3,b
1 implies
(a3 . b3,b1,b1) . b
2,b
4 = b
4 ) );
end;
:: deftheorem E13 defines associative ALTCAT_1:def 7 :
for b
1 being non
empty set for b
2 being
ManySortedSet of
[:b1,b1:]for b
3 being
BinComp of b
2 holds
( b
3 is
associative iff for b
4, b
5, b
6, b
7 being
Element of b
1for b
8, b
9, b
10 being
set holds
( ( b
8 in b
2 . b
4,b
5 & b
9 in b
2 . b
5,b
6 & b
10 in b
2 . b
6,b
7 ) implies (
(b3 . b4,b6,b7) . b
10,
((b3 . b4,b5,b6) . b9,b8) = (b3 . b4,b5,b7) . ((b3 . b5,b6,b7) . b10,b9),b
8 ) ) );
:: deftheorem E14 defines with_right_units ALTCAT_1:def 8 :
:: deftheorem E15 defines with_left_units ALTCAT_1:def 9 :
definition
let c
1 be non
empty AltCatStr ;
let c
2, c
3, c
4 be
object of c
1;
assume E16:
(
<^c2,c3^> <> {} &
<^c3,c4^> <> {} )
;
let c
5 be
Morphism of c
2,c
3;
let c
6 be
Morphism of c
3,c
4;
func a
6 * a
5 -> Morphism of a
2,a
4 equals :
E16:
:: ALTCAT_1:def 10
(the Comp of a1 . a2,a3,a4) . a
6,a
5;
coherence
(the Comp of c1 . c2,c3,c4) . c6,c5 is Morphism of c2,c4
proof
reconsider c
7 =
<^c2,c3^>, c
8 =
<^c3,c4^> as non
empty set by E16;
the
Comp of c
1 . [c2,c3,c4] = the
Comp of c
1 . c
2,c
3,c
4
by MULTOP_1:def 1;
then reconsider c
9 = the
Comp of c
1 . c
2,c
3,c
4 as
Function of
[:c8,c7:],
<^c2,c4^> ;
reconsider c
10 = c
6 as
Element of c
8 ;
reconsider c
11 = c
5 as
Element of c
7 ;
c
9 . c
10,c
11 is
Element of
<^c2,c4^>
;
hence
(the Comp of c1 . c2,c3,c4) . c
6,c
5 is
Morphism of c
2,c
4
;
end;
correctness
;
end;
:: deftheorem E16 defines * ALTCAT_1:def 10 :
:: deftheorem E17 defines compositional ALTCAT_1:def 11 :
registration
let c
1, c
2 be
functional set ;
cluster compositional ManySortedSet of
[:a1,a2:];
existence
ex b1 being ManySortedFunction of [:c1,c2:] st b1 is compositional
proof
per cases
not ( not c
1 = {} & not c
2 = {} & not ( c
1 <> {} & c
2 <> {} ) )
;
suppose E18:
( c
1 = {} or c
2 = {} )
;
set c
3 =
[0] [:c1,c2:];
E19:
dom ([0] [:c1,c2:]) = [:c1,c2:]
by PBOOLE:def 3;
[0] [:c1,c2:] is
Function-yielding
then reconsider c
4 =
[0] [:c1,c2:] as
ManySortedFunction of
[:c1,c2:] ;
take
c
4
;
let c
5 be
set ;
:: uses ALTCAT_1:def 11thus
not ( c
5 in dom c
4 & for b
1, b
2 being
Function holds
not ( c
5 = [b2,b1] & c
4 . c
5 = b
1 * b
2 ) )
by E18, E19, ZFMISC_1:113;
end;
suppose
( c
1 <> {} & c
2 <> {} )
;
then reconsider c
3 = c
1, c
4 = c
2 as non
empty functional set ;
deffunc H
1(
Element of c
3,
Element of c
4)
-> set = a
2 * a
1;
consider c
5 being
ManySortedSet of
[:c3,c4:] such that
E18:
for b
1 being
Element of c
3for b
2 being
Element of c
4 holds c
5 . b
1,b
2 = H
1(b
1,b
2)
from ALTCAT_1:sch 2();
c
5 is
Function-yielding
then reconsider c
6 = c
5 as
ManySortedFunction of
[:c1,c2:] ;
take
c
6
;
let c
7 be
set ;
:: uses ALTCAT_1:def 11assume
c
7 in dom c
6
;
then E19:
c
7 in [:c3,c4:]
by PBOOLE:def 3;
then E20:
( c
7 `1 in c
3 & c
7 `2 in c
4 )
by MCART_1:10;
then reconsider c
8 = c
7 `1 , c
9 = c
7 `2 as
Function by FRAENKEL:def 1;
take
c
9
;
take
c
8
;
thus
c
7 = [c8,c9]
by E19, MCART_1:24;
c
7 = [c8,c9]
by E19, MCART_1:24;
hence c
6 . c
7 =
c
6 . c
8,c
9
by BINOP_1:def 1
.=
c
9 * c
8
by E18, E20
;
end;
end;
end;
end;
theorem E18: :: ALTCAT_1:13
proof
let c
1, c
2 be
functional set ;
let c
3 be
compositional ManySortedSet of
[:c1,c2:];
let c
4, c
5 be
Function;
assume E19:
( c
4 in c
1 & c
5 in c
2 )
;
dom c
3 = [:c1,c2:]
by PBOOLE:def 3;
then
[c4,c5] in dom c
3
by E19, ZFMISC_1:106;
then consider c
6, c
7 being
Function such that
E20:
[c4,c5] = [c7,c6]
and
E21:
c
3 . [c4,c5] = c
6 * c
7
by E17;
( c
4 = c
7 & c
5 = c
6 )
by E20, ZFMISC_1:33;
hence
c
3 . c
4,c
5 = c
5 * c
4
by E21, BINOP_1:def 1;
end;
definition
let c
1, c
2 be
functional set ;
func FuncComp a
1,a
2 -> compositional ManySortedFunction of
[:a2,a1:] means :
E19:
:: ALTCAT_1:def 12
verum;
uniqueness
for b1, b2 being compositional ManySortedFunction of [:c2,c1:] holds b1 = b2
proof
let c
3, c
4 be
compositional ManySortedFunction of
[:c2,c1:];
now
let c
5, c
6 be
set ;
assume
( c
5 in c
2 & c
6 in c
1 )
;
then E19:
[c5,c6] in [:c2,c1:]
by ZFMISC_1:106;
then
[c5,c6] in dom c
3
by PBOOLE:def 3;
then consider c
7, c
8 being
Function such that
E20:
[c5,c6] = [c8,c7]
and
E21:
c
3 . [c5,c6] = c
7 * c
8
by E17;
[c5,c6] in dom c
4
by E19, PBOOLE:def 3;
then consider c
9, c
10 being
Function such that
E22:
[c5,c6] = [c10,c9]
and
E23:
c
4 . [c5,c6] = c
9 * c
10
by E17;
( c
8 = c
10 & c
7 = c
9 )
by E20, E22, ZFMISC_1:33;
hence c
3 . c
5,c
6 =
c
4 . [c5,c6]
by E21, E23, BINOP_1:def 1
.=
c
4 . c
5,c
6
by BINOP_1:def 1
;
end;
hence
c
3 = c
4
by E5;
end;
correctness
existence
ex b1 being compositional ManySortedFunction of [:c2,c1:] st
verum;
;
end;
:: deftheorem E19 defines FuncComp ALTCAT_1:def 12 :
theorem E20: :: ALTCAT_1:14