deffunc H₁( Real) -> Element of REAL = In ((integral (((#R (1 / 2)) * (((x `| (dom x)) (#) (x `| (dom x))) + ((y `| (dom y)) (#) (y `| (dom y))))),a,$1)),REAL);
consider l0 being Function of REAL,REAL such that
A1: for t being Element of REAL holds l0 . t = H₁(t) from FUNCT_2:sch 4();
A2: for t being Real holds l0 . t = integral (((#R (1 / 2)) * (((x `| (dom x)) (#) (x `| (dom x))) + ((y `| (dom y)) (#) (y `| (dom y))))),a,t)

proof

let t be Real; :: thesis: l0 . t = integral (((#R (1 / 2)) * (((x `| (dom x)) (#) (x `| (dom x))) + ((y `| (dom y)) (#) (y `| (dom y))))),a,t)
t in REAL by XREAL_0:def 1;
then l0 . t = In ((integral (((#R (1 / 2)) * (((x `| (dom x)) (#) (x `| (dom x))) + ((y `| (dom y)) (#) (y `| (dom y))))),a,t)),REAL) by A1;
hence l0 . t = integral (((#R (1 / 2)) * (((x `| (dom x)) (#) (x `| (dom x))) + ((y `| (dom y)) (#) (y `| (dom y))))),a,t) ; :: thesis: verum

end;

set L = l0 | [.a,b.];
A3: dom l0 = REAL by FUNCT_2:def 1;
reconsider L = l0 | [.a,b.] as PartFunc of REAL,REAL ;
take L ; :: thesis: ( dom L = [.a,b.] & ( for t being Real st t in [.a,b.] holds
L . t = integral (((#R (1 / 2)) * (((x `| (dom x)) (#) (x `| (dom x))) + ((y `| (dom y)) (#) (y `| (dom y))))),a,t) ) )

now :: thesis: for t being Real st t in [.a,b.] holds
L . t = integral (((#R (1 / 2)) * (((x `| (dom x)) (#) (x `| (dom x))) + ((y `| (dom y)) (#) (y `| (dom y))))),a,t)

let t be Real; :: thesis: ( t in [.a,b.] implies L . t = integral (((#R (1 / 2)) * (((x `| (dom x)) (#) (x `| (dom x))) + ((y `| (dom y)) (#) (y `| (dom y))))),a,t) )
assume t in [.a,b.] ; :: thesis: L . t = integral (((#R (1 / 2)) * (((x `| (dom x)) (#) (x `| (dom x))) + ((y `| (dom y)) (#) (y `| (dom y))))),a,t)
hence L . t = l0 . t by FUNCT_1:49
.= integral (((#R (1 / 2)) * (((x `| (dom x)) (#) (x `| (dom x))) + ((y `| (dom y)) (#) (y `| (dom y))))),a,t) by A2 ;
:: thesis: verum

end;

hence ( dom L = [.a,b.] & ( for t being Real st t in [.a,b.] holds
L . t = integral (((#R (1 / 2)) * (((x `| (dom x)) (#) (x `| (dom x))) + ((y `| (dom y)) (#) (y `| (dom y))))),a,t) ) ) by A3, RELAT_1:62; :: thesis: verum