deffunc H_{1}( object ) -> object = $1 `2 ;

A1: 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(A1);

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 = e `2
; :: thesis: verum

A1: 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 A2: 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;

hence H_{1}(x) in the carrier of S
by A2, MCART_1:10; :: thesis: verum

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

InducedEdges S c= [: the carrier' of S, the carrier of S:] by Th1;

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