deffunc H1( object ) -> object = [$1,$1];
ex f being Function st
( dom f = X & ( for x being object st x in X holds
f . x = H1(x) ) )
from FUNCT_1:sch 3();
hence
ex b1 being Function st
( dom b1 = X & ( for x being object st x in X holds
b1 . x = [x,x] ) )
; verum