now :: thesis: for x being object st x in the_Source_of S holds
x is Function

let x be object ; :: thesis: ( x in the_Source_of S implies x is Function )
assume x in the_Source_of S ; :: thesis: x is Function
then consider G being _Graph such that
A1: ( G in S & x = the_Source_of G ) by Def16;
thus x is Function by A1; :: thesis: verum

end;

hence the_Source_of S is functional by FUNCT_1:def 13; :: thesis: verum