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