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₁ 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