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 = e `2 ) & ( for e being object st e in InducedEdges S holds
F2 . e = e `2 ) implies F1 = F2 )
assume that
A3: for e being object st e in InducedEdges S holds
F1 . e = e `2 and
A4: for e being object st e in InducedEdges S holds
F2 . e = e `2 ; :: thesis: F1 = F2

A5: 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 A6: x in InducedEdges S ; :: thesis: F1 . x = F2 . x
then F1 . x = x `2 by A3;
hence F1 . x = F2 . x by A4, A6; :: 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 A5, FUNCT_1:2; :: thesis: verum