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

now

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

end;

then A5: ( dom F1 = InducedEdges S & dom F2 = InducedEdges S ) by FUNCT_2:def 1;

now

let x be set ; :: thesis: ( x in InducedEdges S implies F1 . x = F2 . x )
assume x in InducedEdges S ; :: thesis: F1 . x = F2 . x
then ( F1 . x = x `2 & F2 . x = x `2 ) by A3, A4;
hence F1 . x = F2 . x ; :: thesis: verum

end;

hence F1 = F2 by A5, FUNCT_1:9; :: thesis: verum