let C be CategoryStr ; :: thesis: for a, b being Object of C
for f being Morphism of a,b st Hom (a,b) <> {} holds
ex f1, f2 being morphism of C st
( a = f1 & b = f2 & f |> f1 & f2 |> f )
let a, b be Object of C; :: thesis: for f being Morphism of a,b st Hom (a,b) <> {} holds
ex f1, f2 being morphism of C st
( a = f1 & b = f2 & f |> f1 & f2 |> f )
let f be Morphism of a,b; :: thesis: ( Hom (a,b) <> {} implies ex f1, f2 being morphism of C st
( a = f1 & b = f2 & f |> f1 & f2 |> f ) )
assume Hom (a,b) <> {} ; :: thesis: ex f1, f2 being morphism of C st
( a = f1 & b = f2 & f |> f1 & f2 |> f )
then f in Hom (a,b) by Def3;
then consider f11 being morphism of C such that
A1: ( f11 = f & ex f1, f2 being morphism of C st
( a = f1 & b = f2 & f11 |> f1 & f2 |> f11 ) ) ;
thus ex f1, f2 being morphism of C st
( a = f1 & b = f2 & f |> f1 & f2 |> f ) by A1; :: thesis: verum