deffunc H_{1}( Element of R) -> Element of bool the carrier of R = In ((Coim ( the InternalRel of R,$1)),(bool the carrier of R));

consider f being Function of the carrier of R,(bool the carrier of R) such that

A1: for x being Element of R holds f . x = H_{1}(x)
from FUNCT_2:sch 4();

take f ; :: thesis: for x being Element of R holds f . x = Coim ( the InternalRel of R,x)

let x be Element of R; :: thesis: f . x = Coim ( the InternalRel of R,x)

A2: f . x = In ((Coim ( the InternalRel of R,x)),(bool the carrier of R)) by A1;

the InternalRel of R " {x} c= the carrier of R ;

hence f . x = Coim ( the InternalRel of R,x) by A2; :: thesis: verum

consider f being Function of the carrier of R,(bool the carrier of R) such that

A1: for x being Element of R holds f . x = H

take f ; :: thesis: for x being Element of R holds f . x = Coim ( the InternalRel of R,x)

let x be Element of R; :: thesis: f . x = Coim ( the InternalRel of R,x)

A2: f . x = In ((Coim ( the InternalRel of R,x)),(bool the carrier of R)) by A1;

the InternalRel of R " {x} c= the carrier of R ;

hence f . x = Coim ( the InternalRel of R,x) by A2; :: thesis: verum