deffunc H_{1}( object ) -> set = the ResultSort of S . ($1 `1);

A7: for x being object st x in InducedEdges S holds

H_{1}(x) in the carrier of S

for x being object st x in InducedEdges S holds

f . x = H_{1}(x)
from FUNCT_2:sch 2(A7);

hence ex b_{1} being Function of (InducedEdges S), the carrier of S st

for e being object st e in InducedEdges S holds

b_{1} . e = the ResultSort of S . (e `1)
; :: thesis: verum

A7: for x being object st x in InducedEdges S holds

H

proof

ex f being Function of (InducedEdges S), the carrier of S st
let x be object ; :: thesis: ( x in InducedEdges S implies H_{1}(x) in the carrier of S )

assume A8: x in InducedEdges S ; :: thesis: H_{1}(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_{1}(x) in the carrier of S
by FUNCT_2:5; :: thesis: verum

end;assume A8: x in InducedEdges S ; :: thesis: H

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

for x being object st x in InducedEdges S holds

f . x = H

hence ex b

for e being object st e in InducedEdges S holds

b