let F1, F2 be Function of (), 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:
then [: the carrier' of S, the carrier of S:] is empty by ZFMISC_1:90;
hence InducedEdges S is empty by ; :: thesis: verum
end;
then ( dom F1 = InducedEdges S & dom F2 = InducedEdges S ) by FUNCT_2:def 1;
hence F1 = F2 by ; :: thesis: verum