let C be non empty AltCatStr ; :: thesis: 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 ; :: thesis: ( 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) ; :: thesis: 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 ; :: thesis: ex o2 being Object of C st
( o1 = a & o2 = b & f in <^o1,o2^> & f is Morphism of o1,o2 )
take o2 ; :: thesis: ( 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; :: thesis: verum