let A, B be non empty transitive AltCatStr ; :: thesis: ( A,B are_opposite & A is with_units implies B is with_units )
assume A1:
A,B are_opposite
; :: thesis: ( not A is with_units or B is with_units )
assume
A is with_units
; :: thesis: B is with_units
then reconsider A = A as non empty transitive with_units AltCatStr ;
deffunc H1( set , set , set , set , set ) -> set = (the Comp of A . $3,$2,$1) . $4,$5;
A2:
now let a,
b,
c be
object of
B;
:: thesis: ( <^a,b^> <> {} & <^b,c^> <> {} implies for f being Morphism of a,b
for g being Morphism of b,c holds g * f = H1(a,b,c,f,g) )assume that A3:
<^a,b^> <> {}
and A4:
<^b,c^> <> {}
;
:: thesis: for f being Morphism of a,b
for g being Morphism of b,c holds g * f = H1(a,b,c,f,g)let f be
Morphism of
a,
b;
:: thesis: for g being Morphism of b,c holds g * f = H1(a,b,c,f,g)let g be
Morphism of
b,
c;
:: thesis: g * f = H1(a,b,c,f,g)reconsider a' =
a,
b' =
b,
c' =
c as
object of
A by A1, Th6;
A5:
<^a,b^> = <^b',a'^>
by A1, Th7;
A6:
<^b,c^> = <^c',b'^>
by A1, Th7;
reconsider f' =
f as
Morphism of
b',
a' by A1, Th7;
reconsider g' =
g as
Morphism of
c',
b' by A1, Th7;
thus g * f =
f' * g'
by A1, A3, A4, Th9
.=
H1(
a,
b,
c,
f,
g)
by A3, A4, A5, A6, ALTCAT_1:def 10
;
:: thesis: verum end;
A7:
now let a be
object of
B;
:: thesis: ex f being set st
( f in <^a,a^> & ( for b being object of B
for g being set st g in <^a,b^> holds
H1(a,a,b,f,g) = g ) )reconsider a' =
a as
object of
A by A1, Th6;
reconsider f =
idm a' as
set ;
take f =
f;
:: thesis: ( f in <^a,a^> & ( for b being object of B
for g being set st g in <^a,b^> holds
H1(a,a,b,f,g) = g ) )
idm a' in <^a',a'^>
;
hence
f in <^a,a^>
by A1, Th7;
:: thesis: for b being object of B
for g being set st g in <^a,b^> holds
H1(a,a,b,f,g) = glet b be
object of
B;
:: thesis: for g being set st g in <^a,b^> holds
H1(a,a,b,f,g) = glet g be
set ;
:: thesis: ( g in <^a,b^> implies H1(a,a,b,f,g) = g )reconsider b' =
b as
object of
A by A1, Th6;
assume A8:
g in <^a,b^>
;
:: thesis: H1(a,a,b,f,g) = gthen A9:
g in <^b',a'^>
by A1, Th7;
reconsider g' =
g as
Morphism of
b',
a' by A1, A8, Th7;
thus H1(
a,
a,
b,
f,
g) =
(idm a') * g'
by A9, ALTCAT_1:def 10
.=
g
by A9, ALTCAT_1:24
;
:: thesis: verum end;
A10:
now let a be
object of
B;
:: thesis: ex f being set st
( f in <^a,a^> & ( for b being object of B
for g being set st g in <^b,a^> holds
H1(b,a,a,g,f) = g ) )reconsider a' =
a as
object of
A by A1, Th6;
reconsider f =
idm a' as
set ;
take f =
f;
:: thesis: ( f in <^a,a^> & ( for b being object of B
for g being set st g in <^b,a^> holds
H1(b,a,a,g,f) = g ) )
idm a' in <^a',a'^>
;
hence
f in <^a,a^>
by A1, Th7;
:: thesis: for b being object of B
for g being set st g in <^b,a^> holds
H1(b,a,a,g,f) = glet b be
object of
B;
:: thesis: for g being set st g in <^b,a^> holds
H1(b,a,a,g,f) = glet g be
set ;
:: thesis: ( g in <^b,a^> implies H1(b,a,a,g,f) = g )reconsider b' =
b as
object of
A by A1, Th6;
assume A11:
g in <^b,a^>
;
:: thesis: H1(b,a,a,g,f) = gthen A12:
g in <^a',b'^>
by A1, Th7;
reconsider g' =
g as
Morphism of
a',
b' by A1, A11, Th7;
thus H1(
b,
a,
a,
g,
f) =
g' * (idm a')
by A12, ALTCAT_1:def 10
.=
g
by A12, ALTCAT_1:def 19
;
:: thesis: verum end;
thus
B is with_units
from YELLOW18:sch 3(A2, A7, A10); :: thesis: verum