let A, B be non empty transitive AltCatStr ; :: thesis: ( A,B have_the_same_composition iff for a1, a2, a3 being object of A st <^a1,a2^> <> {} & <^a2,a3^> <> {} holds
for b1, b2, b3 being object of B st <^b1,b2^> <> {} & <^b2,b3^> <> {} & b1 = a1 & b2 = a2 & b3 = a3 holds
for f1 being Morphism of a1,a2
for g1 being Morphism of b1,b2 st g1 = f1 holds
for f2 being Morphism of a2,a3
for g2 being Morphism of b2,b3 st g2 = f2 holds
f2 * f1 = g2 * g1 )
hereby :: thesis: ( ( for a1, a2, a3 being object of A st <^a1,a2^> <> {} & <^a2,a3^> <> {} holds
for b1, b2, b3 being object of B st <^b1,b2^> <> {} & <^b2,b3^> <> {} & b1 = a1 & b2 = a2 & b3 = a3 holds
for f1 being Morphism of a1,a2
for g1 being Morphism of b1,b2 st g1 = f1 holds
for f2 being Morphism of a2,a3
for g2 being Morphism of b2,b3 st g2 = f2 holds
f2 * f1 = g2 * g1 ) implies A,B have_the_same_composition )
assume A1:
A,
B have_the_same_composition
;
:: thesis: for a1, a2, a3 being object of A st <^a1,a2^> <> {} & <^a2,a3^> <> {} holds
for b1, b2, b3 being object of B st <^b1,b2^> <> {} & <^b2,b3^> <> {} & b1 = a1 & b2 = a2 & b3 = a3 holds
for f1 being Morphism of a1,a2
for g1 being Morphism of b1,b2 st g1 = f1 holds
for f2 being Morphism of a2,a3
for g2 being Morphism of b2,b3 st g2 = f2 holds
f2 * f1 = g2 * g1let a1,
a2,
a3 be
object of
A;
:: thesis: ( <^a1,a2^> <> {} & <^a2,a3^> <> {} implies for b1, b2, b3 being object of B st <^b1,b2^> <> {} & <^b2,b3^> <> {} & b1 = a1 & b2 = a2 & b3 = a3 holds
for f1 being Morphism of a1,a2
for g1 being Morphism of b1,b2 st g1 = f1 holds
for f2 being Morphism of a2,a3
for g2 being Morphism of b2,b3 st g2 = f2 holds
f2 * f1 = g2 * g1 )assume A2:
(
<^a1,a2^> <> {} &
<^a2,a3^> <> {} )
;
:: thesis: for b1, b2, b3 being object of B st <^b1,b2^> <> {} & <^b2,b3^> <> {} & b1 = a1 & b2 = a2 & b3 = a3 holds
for f1 being Morphism of a1,a2
for g1 being Morphism of b1,b2 st g1 = f1 holds
for f2 being Morphism of a2,a3
for g2 being Morphism of b2,b3 st g2 = f2 holds
f2 * f1 = g2 * g1let b1,
b2,
b3 be
object of
B;
:: thesis: ( <^b1,b2^> <> {} & <^b2,b3^> <> {} & b1 = a1 & b2 = a2 & b3 = a3 implies for f1 being Morphism of a1,a2
for g1 being Morphism of b1,b2 st g1 = f1 holds
for f2 being Morphism of a2,a3
for g2 being Morphism of b2,b3 st g2 = f2 holds
f2 * f1 = g2 * g1 )assume that A3:
(
<^b1,b2^> <> {} &
<^b2,b3^> <> {} )
and A4:
(
b1 = a1 &
b2 = a2 &
b3 = a3 )
;
:: thesis: for f1 being Morphism of a1,a2
for g1 being Morphism of b1,b2 st g1 = f1 holds
for f2 being Morphism of a2,a3
for g2 being Morphism of b2,b3 st g2 = f2 holds
f2 * f1 = g2 * g1let f1 be
Morphism of
a1,
a2;
:: thesis: for g1 being Morphism of b1,b2 st g1 = f1 holds
for f2 being Morphism of a2,a3
for g2 being Morphism of b2,b3 st g2 = f2 holds
f2 * f1 = g2 * g1let g1 be
Morphism of
b1,
b2;
:: thesis: ( g1 = f1 implies for f2 being Morphism of a2,a3
for g2 being Morphism of b2,b3 st g2 = f2 holds
f2 * f1 = g2 * g1 )assume A5:
g1 = f1
;
:: thesis: for f2 being Morphism of a2,a3
for g2 being Morphism of b2,b3 st g2 = f2 holds
f2 * f1 = g2 * g1let f2 be
Morphism of
a2,
a3;
:: thesis: for g2 being Morphism of b2,b3 st g2 = f2 holds
f2 * f1 = g2 * g1let g2 be
Morphism of
b2,
b3;
:: thesis: ( g2 = f2 implies f2 * f1 = g2 * g1 )assume A6:
g2 = f2
;
:: thesis: f2 * f1 = g2 * g1A7:
( the
Comp of
A . a1,
a2,
a3 = the
Comp of
A . [a1,a2,a3] & the
Comp of
B . b1,
b2,
b3 = the
Comp of
B . [b1,b2,b3] )
by MULTOP_1:def 1;
( the
Comp of
A . a1,
a2,
a3 is
Function of
[:<^a2,a3^>,<^a1,a2^>:],
<^a1,a3^> &
<^a1,a3^> <> {} & the
Comp of
B . b1,
b2,
b3 is
Function of
[:<^b2,b3^>,<^b1,b2^>:],
<^b1,b3^> &
<^b1,b3^> <> {} )
by A2, A3, ALTCAT_1:def 4;
then
(
dom (the Comp of A . a1,a2,a3) = [:<^a2,a3^>,<^a1,a2^>:] &
dom (the Comp of B . b1,b2,b3) = [:<^b2,b3^>,<^b1,b2^>:] )
by FUNCT_2:def 1;
then A8:
(
[f2,f1] in dom (the Comp of A . a1,a2,a3) &
[g2,g1] in dom (the Comp of B . b1,b2,b3) )
by A2, A3, ZFMISC_1:def 2;
thus f2 * f1 =
(the Comp of A . a1,a2,a3) . f2,
f1
by A2, ALTCAT_1:def 10
.=
(the Comp of B . b1,b2,b3) . g2,
g1
by A1, A4, A5, A6, A7, A8, Th10
.=
g2 * g1
by A3, ALTCAT_1:def 10
;
:: thesis: verum
end;
assume A9:
for a1, a2, a3 being object of A st <^a1,a2^> <> {} & <^a2,a3^> <> {} holds
for b1, b2, b3 being object of B st <^b1,b2^> <> {} & <^b2,b3^> <> {} & b1 = a1 & b2 = a2 & b3 = a3 holds
for f1 being Morphism of a1,a2
for g1 being Morphism of b1,b2 st g1 = f1 holds
for f2 being Morphism of a2,a3
for g2 being Morphism of b2,b3 st g2 = f2 holds
f2 * f1 = g2 * g1
; :: thesis: A,B have_the_same_composition
let a1, a2, a3, x be set ; :: according to PARTFUN1:def 6,YELLOW20:def 1 :: thesis: ( not x in (dom (the Comp of A . [a1,a2,a3])) /\ (dom (the Comp of B . [a1,a2,a3])) or (the Comp of A . [a1,a2,a3]) . x = (the Comp of B . [a1,a2,a3]) . x )
assume
x in (dom (the Comp of A . [a1,a2,a3])) /\ (dom (the Comp of B . [a1,a2,a3]))
; :: thesis: (the Comp of A . [a1,a2,a3]) . x = (the Comp of B . [a1,a2,a3]) . x
then A10:
( x in dom (the Comp of A . [a1,a2,a3]) & x in dom (the Comp of B . [a1,a2,a3]) )
by XBOOLE_0:def 4;
then
( [a1,a2,a3] in dom the Comp of A & [a1,a2,a3] in dom the Comp of B )
by FUNCT_1:def 4, RELAT_1:60;
then A11:
( [a1,a2,a3] in [:the carrier of A,the carrier of A,the carrier of A:] & [a1,a2,a3] in [:the carrier of B,the carrier of B,the carrier of B:] )
by PARTFUN1:def 4;
then reconsider a1 = a1, a2 = a2, a3 = a3 as object of A by MCART_1:73;
reconsider b1 = a1, b2 = a2, b3 = a3 as object of B by A11, MCART_1:73;
A12:
( the Comp of A . a1,a2,a3 = the Comp of A . [a1,a2,a3] & the Comp of B . b1,b2,b3 = the Comp of B . [b1,b2,b3] )
by MULTOP_1:def 1;
then
( ( [:<^a2,a3^>,<^a1,a2^>:] <> {} implies <^a1,a3^> <> {} ) & ( [:<^b2,b3^>,<^b1,b2^>:] <> {} implies <^b1,b3^> <> {} ) )
by A10;
then A13:
( dom (the Comp of A . a1,a2,a3) = [:<^a2,a3^>,<^a1,a2^>:] & dom (the Comp of B . b1,b2,b3) = [:<^b2,b3^>,<^b1,b2^>:] )
by FUNCT_2:def 1;
then consider f2, f1 being set such that
A14:
( f2 in <^a2,a3^> & f1 in <^a1,a2^> & x = [f2,f1] )
by A10, A12, ZFMISC_1:def 2;
reconsider f2 = f2 as Morphism of a2,a3 by A14;
reconsider f1 = f1 as Morphism of a1,a2 by A14;
A15:
( f1 in <^b1,b2^> & f2 in <^b2,b3^> )
by A10, A12, A13, A14, ZFMISC_1:106;
reconsider g1 = f1 as Morphism of b1,b2 by A10, A12, A13, A14, ZFMISC_1:106;
reconsider g2 = f2 as Morphism of b2,b3 by A10, A12, A13, A14, ZFMISC_1:106;
(the Comp of A . [a1,a2,a3]) . x =
(the Comp of A . a1,a2,a3) . f2,f1
by A14, MULTOP_1:def 1
.=
f2 * f1
by A14, ALTCAT_1:def 10
.=
g2 * g1
by A9, A14, A15
.=
(the Comp of B . b1,b2,b3) . g2,g1
by A15, ALTCAT_1:def 10
;
hence
(the Comp of A . [a1,a2,a3]) . x = (the Comp of B . [a1,a2,a3]) . x
by A14, MULTOP_1:def 1; :: thesis: verum