defpred S₁[ GroupMorphism, GroupMorphism] means dom $1 = cod $2;
let g, f be GroupMorphism; :: thesis: ( dom g = cod f implies ex G1, G2, G3 being AddGroup st
( g is Morphism of G2,G3 & f is Morphism of G1,G2 ) )
assume A1: S₁[g,f] ; :: thesis: ex G1, G2, G3 being AddGroup st
( g is Morphism of G2,G3 & f is Morphism of G1,G2 )
consider G2, G3 being AddGroup such that
A2: g is Morphism of G2,G3 by Th24;
A3: G2 = dom g by A2, Def19;
consider G1, G2' being AddGroup such that
A4: f is Morphism of G1,G2' by Th24;
G2' = cod f by A4, Def19;
hence ex G1, G2, G3 being AddGroup st
( g is Morphism of G2,G3 & f is Morphism of G1,G2 ) by A1, A2, A3, A4; :: thesis: verum