let f1, f2 be PartFunc of REAL,REAL; :: thesis: ( dom f1 = [.a,b.] & ( for t being Real st t in [.a,b.] holds
f1 . t = integral (((#R (1 / 2)) * (((x `| (dom x)) (#) (x `| (dom x))) + ((y `| (dom y)) (#) (y `| (dom y))))),a,t) ) & dom f2 = [.a,b.] & ( for t being Real st t in [.a,b.] holds
f2 . t = integral (((#R (1 / 2)) * (((x `| (dom x)) (#) (x `| (dom x))) + ((y `| (dom y)) (#) (y `| (dom y))))),a,t) ) implies f1 = f2 )
assume that
A4: ( dom f1 = [.a,b.] & ( for t being Real st t in [.a,b.] holds
f1 . t = integral (((#R (1 / 2)) * (((x `| (dom x)) (#) (x `| (dom x))) + ((y `| (dom y)) (#) (y `| (dom y))))),a,t) ) ) and
A5: ( dom f2 = [.a,b.] & ( for t being Real st t in [.a,b.] holds
f2 . t = integral (((#R (1 / 2)) * (((x `| (dom x)) (#) (x `| (dom x))) + ((y `| (dom y)) (#) (y `| (dom y))))),a,t) ) ) ; :: thesis: f1 = f2

now :: thesis: for t being object st t in dom f1 holds
f1 . t = f2 . t

let t be object ; :: thesis: ( t in dom f1 implies f1 . t = f2 . t )
assume A6: t in dom f1 ; :: thesis: f1 . t = f2 . t
then reconsider s = t as Real ;
thus f1 . t = integral (((#R (1 / 2)) * (((x `| (dom x)) (#) (x `| (dom x))) + ((y `| (dom y)) (#) (y `| (dom y))))),a,s) by A4, A6
.= f2 . t by A4, A5, A6 ; :: thesis: verum

end;

hence f1 = f2 by A4, A5, FUNCT_1:2; :: thesis: verum