defpred S₁[ object , object ] means ( ( $1 in A implies $2 = +infty ) & ( not $1 in A implies $2 = 0 ) );
A1: for x being object st x in X holds
ex y being object st S₁[x,y]

proof

let x be object ; :: thesis: ( x in X implies ex y being object st S₁[x,y] )
assume x in X ; :: thesis: ex y being object st S₁[x,y]
( not x in A implies ex y being object st
( y = {} & ( x in A implies y = +infty ) & ( not x in A implies y = {} ) ) ) ;
hence ex y being object st S₁[x,y] ; :: thesis: verum

end;

A2: for x, y1, y2 being object st x in X & S₁[x,y1] & S₁[x,y2] holds
y1 = y2 ;
consider f being Function such that
A3: ( dom f = X & ( for x being object st x in X holds
S₁[x,f . x] ) ) from FUNCT_1:sch 2(A2, A1);
for x being object st x in X holds
f . x in ExtREAL

proof

let x be object ; :: thesis: ( x in X implies f . x in ExtREAL )
assume A4: x in X ; :: thesis: f . x in ExtREAL

per cases ( x in A or not x in A ) ;

suppose x in A ; :: thesis: f . x in ExtREAL

then f . x = +infty by A3, A4;
hence f . x in ExtREAL ; :: thesis: verum

end;

suppose not x in A ; :: thesis: f . x in ExtREAL

then f . x = 0. by A3, A4;
hence f . x in ExtREAL ; :: thesis: verum

end;

end;

end;

then reconsider f = f as Function of X,ExtREAL by A3, FUNCT_2:3;
take f ; :: thesis: for x being object st x in X holds
( ( x in A implies f . x = +infty ) & ( not x in A implies f . x = 0 ) )
thus for x being object st x in X holds
( ( x in A implies f . x = +infty ) & ( not x in A implies f . x = 0 ) ) by A3; :: thesis: verum