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

proof

let x be object ; :: thesis: ( x in InducedEdges S implies H₁(x) in the carrier of S )
assume A8: 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;
then ( x `1 in the carrier' of S & x `2 in the carrier of S ) by A8, MCART_1:10;
hence H₁(x) in the carrier of S by FUNCT_2:5; :: thesis: verum

end;

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