consider e being Element of product the Sorts of MSA;
set p = e | (InputVertices S);
A1: ( dom the Sorts of MSA = the carrier of S & ex g being Function st
( e = g & dom g = dom the Sorts of MSA & ( for x being set st x in dom the Sorts of MSA holds
g . x in the Sorts of MSA . x ) ) ) by CARD_3:def 5, PARTFUN1:def 4;
then dom (e | (InputVertices S)) = InputVertices S by RELAT_1:91;
then reconsider p = e | (InputVertices S) as ManySortedSet of InputVertices S by PARTFUN1:def 4, RELAT_1:def 18;
take p ; :: thesis: for v being Vertex of S st v in InputVertices S holds
p . v in the Sorts of MSA . v
let v be Vertex of S; :: thesis: ( v in InputVertices S implies p . v in the Sorts of MSA . v )
assume v in InputVertices S ; :: thesis: p . v in the Sorts of MSA . v
then p . v = e . v by FUNCT_1:72;
hence p . v in the Sorts of MSA . v by A1; :: thesis: verum