deffunc H₁( Subset of T) -> Element of bool the carrier of T = Cl_Seq $1;
consider f being map of T such that
A1: for A being Subset of T holds f . A = H₁(A) from FUNCT_2:sch 4();
take f ; :: thesis: for A being Subset of T holds f . A = Cl_Seq A
let A be Subset of T; :: thesis: f . A = Cl_Seq A
thus f . A = Cl_Seq A by A1; :: thesis: verum