now :: thesis: for x being object st x in the_Target_of S holds
x is Function
let x be object ; :: thesis: ( x in the_Target_of S implies x is Function )
assume x in the_Target_of S ; :: thesis: x is Function
then consider G being _Graph such that
A2: ( G in S & x = the_Target_of G ) by Def17;
thus x is Function by A2; :: thesis: verum
end;
hence the_Target_of S is functional by FUNCT_1:def 13; :: thesis: verum