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