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

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

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

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;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

now :: thesis: ( the carrier of S is empty implies InducedEdges S is empty )

then
( dom F1 = InducedEdges S & dom F2 = InducedEdges S )
by FUNCT_2:def 1;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 [: 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

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