deffunc H₁( set ) -> set = $1 `2 ;
A1: for x being set st x in InducedEdges S holds
H₁(x) in the carrier of S

proof

let x be set ; :: thesis: ( x in InducedEdges S implies H₁(x) in the carrier of S )
assume A2: x in InducedEdges S ; :: thesis: H₁(x) in the carrier of S
InducedEdges S c= [: the carrier' of S, the carrier of S:] by Th1;
hence H₁(x) in the carrier of S by A2, MCART_1:10; :: thesis: verum

end;

ex f being Function of (InducedEdges S), the carrier of S st
for x being set st x in InducedEdges S holds
f . x = H₁(x) from FUNCT_2:sch 2(A1);
hence ex b₁ being Function of (InducedEdges S), the carrier of S st
for e being set st e in InducedEdges S holds
b₁ . e = e `2 ; :: thesis: verum