A2:
dom (f | A) = A
by A1, RELAT_1:62;

rng (f | A) c= the carrier of X ;

then reconsider g = f | A as Function of A, the carrier of X by A2, FUNCT_2:2;

integral g is Point of X ;

hence ( ex b_{1} being Element of X ex g being Function of A, the carrier of X st

( g = f | A & b_{1} = integral g ) & ( for b_{1}, b_{2} being Element of X st ex g being Function of A, the carrier of X st

( g = f | A & b_{1} = integral g ) & ex g being Function of A, the carrier of X st

( g = f | A & b_{2} = integral g ) holds

b_{1} = b_{2} ) )
; :: thesis: verum

rng (f | A) c= the carrier of X ;

then reconsider g = f | A as Function of A, the carrier of X by A2, FUNCT_2:2;

integral g is Point of X ;

hence ( ex b

( g = f | A & b

( g = f | A & b

( g = f | A & b

b