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 H₁( set , set , set , set , set ) -> set = ( the Comp of A . ($3,$2,$1)) . ($4,$5);

A2: now :: thesis: for a, b, c being Object of B st <^a,b^> <> {} & <^b,c^> <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c holds g * f = H₁(a,b,c,f,g)

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 = H₁(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 = H₁(a,b,c,f,g)
let f be Morphism of a,b; :: thesis: for g being Morphism of b,c holds g * f = H₁(a,b,c,f,g)
let g be Morphism of b,c; :: thesis: g * f = H₁(a,b,c,f,g)
reconsider a9 = a, b9 = b, c9 = c as Object of A by A1;
A5: <^a,b^> = <^b9,a9^> by A1, Th7;
A6: <^b,c^> = <^c9,b9^> by A1, Th7;
reconsider f9 = f as Morphism of b9,a9 by A1, Th7;
reconsider g9 = g as Morphism of c9,b9 by A1, Th7;
thus g * f = f9 * g9 by A1, A3, A4, Th9
.= H₁(a,b,c,f,g) by A3, A4, A5, A6, ALTCAT_1:def 8 ; :: thesis: verum

end;

A7: now :: thesis: for a being Object of B 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
H₁(a,a,b,f,g) = g ) )

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
H₁(a,a,b,f,g) = g ) )
reconsider a9 = a as Object of A by A1;
reconsider f = idm a9 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
H₁(a,a,b,f,g) = g ) )
idm a9 in <^a9,a9^> ;
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
H₁(a,a,b,f,g) = g
let b be Object of B; :: thesis: for g being set st g in <^a,b^> holds
H₁(a,a,b,f,g) = g
let g be set ; :: thesis: ( g in <^a,b^> implies H₁(a,a,b,f,g) = g )
reconsider b9 = b as Object of A by A1;
assume A8: g in <^a,b^> ; :: thesis: H₁(a,a,b,f,g) = g
then A9: g in <^b9,a9^> by A1, Th7;
reconsider g9 = g as Morphism of b9,a9 by A1, A8, Th7;
thus H₁(a,a,b,f,g) = (idm a9) * g9 by A9, ALTCAT_1:def 8
.= g by A9, ALTCAT_1:20 ; :: thesis: verum

end;

A10: now :: thesis: for a being Object of B 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
H₁(b,a,a,g,f) = g ) )

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
H₁(b,a,a,g,f) = g ) )
reconsider a9 = a as Object of A by A1;
reconsider f = idm a9 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
H₁(b,a,a,g,f) = g ) )
idm a9 in <^a9,a9^> ;
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
H₁(b,a,a,g,f) = g
let b be Object of B; :: thesis: for g being set st g in <^b,a^> holds
H₁(b,a,a,g,f) = g
let g be set ; :: thesis: ( g in <^b,a^> implies H₁(b,a,a,g,f) = g )
reconsider b9 = b as Object of A by A1;
assume A11: g in <^b,a^> ; :: thesis: H₁(b,a,a,g,f) = g
then A12: g in <^a9,b9^> by A1, Th7;
reconsider g9 = g as Morphism of a9,b9 by A1, A11, Th7;
thus H₁(b,a,a,g,f) = g9 * (idm a9) by A12, ALTCAT_1:def 8
.= g by A12, ALTCAT_1:def 17 ; :: thesis: verum

end;

thus B is with_units from YELLOW18:sch 3(A2, A7, A10); :: thesis: verum