L1: dom (f | A) = A by AS, RELAT_1:91;
rng (f | A) c= the carrier of X ;
then reconsider g = f | A as Function of A,the carrier of X by L1, FUNCT_2:4;
integral g is Point of X ;
hence ( ex b₁ being Element of X ex g being Function of A,the carrier of X st
( g = f | A & b₁ = integral g ) & ( for b₁, b₂ being Element of X st ex g being Function of A,the carrier of X st
( g = f | A & b₁ = integral g ) & ex g being Function of A,the carrier of X st
( g = f | A & b₂ = integral g ) holds
b₁ = b₂ ) ) ; :: thesis: verum