let r1, r2 be Real; :: thesis: ( ( for X being Subset of REAL st X = { |.(x - z).| where z is Element of COMPLEX n : z in A } holds
r1 = lower_bound X ) & ( for X being Subset of REAL st X = { |.(x - z).| where z is Element of COMPLEX n : z in A } holds
r2 = lower_bound X ) implies r1 = r2 )
assume that
A3: for X being Subset of REAL st X = { |.(x - z).| where z is Element of COMPLEX n : z in A } holds
r1 = lower_bound X and
A4: for X being Subset of REAL st X = { |.(x - z).| where z is Element of COMPLEX n : z in A } holds
r2 = lower_bound X ; :: thesis: r1 = r2
deffunc H₁( Element of COMPLEX n) -> Element of REAL = In (|.(x - $1).|,REAL);
deffunc H₂( Element of COMPLEX n) -> Real = |.(x - $1).|;
defpred S₁[ set ] means $1 in A;
reconsider X = { H₁(z) where z is Element of COMPLEX n : S₁[z] } as Subset of REAL from DOMAIN_1:sch 8();
A1: for z being Element of COMPLEX n holds H₁(z) = H₂(z) ;
A2: { H₁(z1) where z1 is Element of COMPLEX n : S₁[z1] } = { H₂(z2) where z2 is Element of COMPLEX n : S₁[z2] } from FRAENKEL:sch 5(A1);
r1 = lower_bound X by A3, A2;
hence r1 = r2 by A4, A2; :: thesis: verum