consider G being Function of (bool REAL),ExtREAL such that
A1: for A being Subset of REAL holds G . A = COMPLEX A from FUNCT_2:sch 4();
 take G ; :: thesis: for A being Subset of REAL holds G . A = inf (Svc A)
for A being Subset of REAL holds G . A = inf (Svc A)
proof
let A be Subset of REAL; :: thesis: G . A = inf (Svc A)
G . A = COMPLEX A by A1;
hence G . A = inf (Svc A) ; :: thesis: verum
end;
hence for A being Subset of REAL holds G . A = inf (Svc A) ; :: thesis: verum