deffunc H₁( Subset of A) -> Element of K10( the carrier of A) = $1 % I;
ex f being Function of (bool the carrier of A),(bool the carrier of A) st
for X being Subset of A holds f . X = H₁(X) from FUNCT_2:sch 4();
then consider f being Function of (bool the carrier of A),(bool the carrier of A) such that
A1: for X being Subset of A holds f . X = H₁(X) ;
take f ; :: thesis: for x being Subset of A holds f . x = x % I
let r be Subset of A; :: thesis: f . r = r % I
thus f . r = r % I by A1; :: thesis: verum