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 Def13;
then A1: Args ((compsym (a,b,c)),(MSAlg C)) = product <*(Hom (b,c)),(Hom (a,b))*> by Lm5;

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 object such that
A2: ( g in Hom (b,c) & f in Hom (a,b) ) and
A3: x = <*g,f*> by A1, FINSEQ_3:124;
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 A3; :: 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:1; :: thesis: verum

end;

given g, f being Morphism of C such that A4: x = <*g,f*> and
A5: ( 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 A5;
hence x in Args ((compsym (a,b,c)),(MSAlg C)) by A1, A4, FINSEQ_3:124; :: thesis: verum