let F1, F2 be Function of (InducedEdges S),the carrier of S; :: thesis: ( ( for e being set st e in InducedEdges S holds
F1 . e = the ResultSort of S . (e `1 ) ) & ( for e being set st e in InducedEdges S holds
F2 . e = the ResultSort of S . (e `1 ) ) implies F1 = F2 )
assume that
A9: for e being set st e in InducedEdges S holds
F1 . e = the ResultSort of S . (e `1 ) and
A10: for e being set st e in InducedEdges S holds
F2 . e = the ResultSort of S . (e `1 ) ; :: thesis: F1 = F2

A11: now

let x be set ; :: thesis: ( x in InducedEdges S implies F1 . x = F2 . x )
assume A12: x in InducedEdges S ; :: thesis: F1 . x = F2 . x
then F1 . x = the ResultSort of S . (x `1 ) by A9;
hence F1 . x = F2 . x by A10, A12; :: thesis: verum

end;

now

assume the carrier of S is empty ; :: thesis: InducedEdges S is empty
then [:the carrier' of S,the carrier of S:] is empty by ZFMISC_1:113;
hence InducedEdges S is empty by Th1, XBOOLE_1:3; :: thesis: verum

end;

then ( dom F1 = InducedEdges S & dom F2 = InducedEdges S ) by FUNCT_2:def 1;
hence F1 = F2 by A11, FUNCT_1:9; :: thesis: verum