let C be non empty AltCatStr ; for a, b, f being object st f in the Arrows of C . (a,b) holds
ex o1, o2 being Object of C st
( o1 = a & o2 = b & f in <^o1,o2^> & f is Morphism of o1,o2 )
let a, b, f be object ; ( f in the Arrows of C . (a,b) implies ex o1, o2 being Object of C st
( o1 = a & o2 = b & f in <^o1,o2^> & f is Morphism of o1,o2 ) )
assume A1:
f in the Arrows of C . (a,b)
; ex o1, o2 being Object of C st
( o1 = a & o2 = b & f in <^o1,o2^> & f is Morphism of o1,o2 )
then
[a,b] in dom the Arrows of C
by FUNCT_1:def 2;
then
[a,b] in [: the carrier of C, the carrier of C:]
;
then reconsider o1 = a, o2 = b as Object of C by ZFMISC_1:87;
take
o1
; ex o2 being Object of C st
( o1 = a & o2 = b & f in <^o1,o2^> & f is Morphism of o1,o2 )
take
o2
; ( o1 = a & o2 = b & f in <^o1,o2^> & f is Morphism of o1,o2 )
thus
( o1 = a & o2 = b & f in <^o1,o2^> & f is Morphism of o1,o2 )
by A1, ALTCAT_1:def 1; verum