deffunc H1( object ) -> object = $1 `2 ;
A1: for x being object st x in InducedEdges S holds
H1(x) in the carrier of S
proof
let x be object ; :: thesis: ( x in InducedEdges S implies H1(x) in the carrier of S )
assume A2: x in InducedEdges S ; :: thesis: H1(x) in the carrier of S
InducedEdges S c= [: the carrier' of S, the carrier of S:] by Th1;
hence H1(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 object st x in InducedEdges S holds
f . x = H1(x) from FUNCT_2:sch 2(A1);
 hence ex b1 being Function of (InducedEdges S), the carrier of S st
for e being object st e in InducedEdges S holds
b1 . e = e `2 ; :: thesis: verum