let C be non empty AltCatStr ; :: thesis: for a, b, f being set 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 set ; :: 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 4;
then [a,b] in [:the carrier of C,the carrier of C:] by PARTFUN1:def 4;
then reconsider o1 = a, o2 = b as object of C by ZFMISC_1:106;
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 2; :: thesis: verum