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 st
( o1 = a & o2 = b & f in <^o1,o2^> & f is Morphism of , )
let a, b, f be set ; :: thesis: ( f in the Arrows of C . a,b implies ex o1, o2 being object of st
( o1 = a & o2 = b & f in <^o1,o2^> & f is Morphism of , ) )
assume A1: f in the Arrows of C . a,b ; :: thesis: ex o1, o2 being object of st
( o1 = a & o2 = b & f in <^o1,o2^> & f is Morphism of , )
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 by ZFMISC_1:106;
take o1 ; :: thesis: ex o2 being object of st
( o1 = a & o2 = b & f in <^o1,o2^> & f is Morphism of , )
take o2 ; :: thesis: ( o1 = a & o2 = b & f in <^o1,o2^> & f is Morphism of , )
thus ( o1 = a & o2 = b & f in <^o1,o2^> & f is Morphism of , ) by A1, ALTCAT_1:def 2; :: thesis: verum