let F1, F2 be Function of (InducedEdges S), the carrier of S; :: thesis: ( ( for e being object st e in InducedEdges S holds
F1 . e = the ResultSort of S . (e `1) ) & ( for e being object st e in InducedEdges S holds
F2 . e = the ResultSort of S . (e `1) ) implies F1 = F2 )
assume that
A9: for e being object st e in InducedEdges S holds
F1 . e = the ResultSort of S . (e `1) and
A10: for e being object st e in InducedEdges S holds
F2 . e = the ResultSort of S . (e `1) ; :: thesis: F1 = F2
A11: now :: thesis: for x being object st x in InducedEdges S holds
F1 . x = F2 . x
let x be object ; :: 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 :: thesis: ( the carrier of S is empty implies InducedEdges S is empty )
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:90;
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:2; :: thesis: verum