set e = the Element of product the Sorts of MSA;

set p = the Element of product the Sorts of MSA | (InputVertices S);

A1: ( dom the Sorts of MSA = the carrier of S & ex g being Function st

( the Element of product the Sorts of MSA = g & dom g = dom the Sorts of MSA & ( for x being object st x in dom the Sorts of MSA holds

g . x in the Sorts of MSA . x ) ) ) by CARD_3:def 5, PARTFUN1:def 2;

reconsider p = the Element of product the Sorts of MSA | (InputVertices S) as ManySortedSet of InputVertices S ;

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 = the Element of product the Sorts of MSA . v by FUNCT_1:49;

hence p . v in the Sorts of MSA . v by A1; :: thesis: verum

set p = the Element of product the Sorts of MSA | (InputVertices S);

A1: ( dom the Sorts of MSA = the carrier of S & ex g being Function st

( the Element of product the Sorts of MSA = g & dom g = dom the Sorts of MSA & ( for x being object st x in dom the Sorts of MSA holds

g . x in the Sorts of MSA . x ) ) ) by CARD_3:def 5, PARTFUN1:def 2;

reconsider p = the Element of product the Sorts of MSA | (InputVertices S) as ManySortedSet of InputVertices S ;

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 = the Element of product the Sorts of MSA . v by FUNCT_1:49;

hence p . v in the Sorts of MSA . v by A1; :: thesis: verum