let C be Category; :: thesis: for a, b, c being Object of C
for x being set holds
( x in Args (compsym a,b,c),(MSAlg C) iff ex g, f being Morphism of C st
( x = <*g,f*> & dom f = a & cod f = b & dom g = b & cod g = c ) )
let a, b, c be Object of C; :: thesis: for x being set holds
( x in Args (compsym a,b,c),(MSAlg C) iff ex g, f being Morphism of C st
( x = <*g,f*> & dom f = a & cod f = b & dom g = b & cod g = c ) )
let x be set ; :: thesis: ( x in Args (compsym a,b,c),(MSAlg C) iff ex g, f being Morphism of C st
( x = <*g,f*> & dom f = a & cod f = b & dom g = b & cod g = c ) )
set A = MSAlg C;
for a, b being Object of C holds the Sorts of (MSAlg C) . (homsym a,b) = Hom a,b by Def15;
then A1: Args (compsym a,b,c),(MSAlg C) = product <*(Hom b,c),(Hom a,b)*> by Lm3;

hereby :: thesis: ( ex g, f being Morphism of C st
( x = <*g,f*> & dom f = a & cod f = b & dom g = b & cod g = c ) implies x in Args (compsym a,b,c),(MSAlg C) )

assume x in Args (compsym a,b,c),(MSAlg C) ; :: thesis: ex g, f being Morphism of C st
( x = <*g,f*> & dom f = a & cod f = b & dom g = b & cod g = c )
then consider g, f being set such that
A2: ( g in Hom b,c & f in Hom a,b & x = <*g,f*> ) by A1, FUNCT_6:2;
reconsider g = g, f = f as Morphism of C by A2;
take g = g; :: thesis: ex f being Morphism of C st
( x = <*g,f*> & dom f = a & cod f = b & dom g = b & cod g = c )
take f = f; :: thesis: ( x = <*g,f*> & dom f = a & cod f = b & dom g = b & cod g = c )
thus x = <*g,f*> by A2; :: thesis: ( dom f = a & cod f = b & dom g = b & cod g = c )
thus ( dom f = a & cod f = b & dom g = b & cod g = c ) by A2, CAT_1:18; :: thesis: verum

end;

given g, f being Morphism of C such that A3: ( x = <*g,f*> & dom f = a & cod f = b & dom g = b & cod g = c ) ; :: thesis: x in Args (compsym a,b,c),(MSAlg C)
( f in Hom a,b & g in Hom b,c ) by A3, CAT_1:18;
hence x in Args (compsym a,b,c),(MSAlg C) by A1, A3, FUNCT_6:2; :: thesis: verum