set n = Char R;
defpred S₁[ object , object ] means ex a being Element of R st
( $1 = a & $2 = a |^ (Char R) );

A: now :: thesis: for x being object st x in the carrier of R holds
ex y being object st
( y in the carrier of R & S₁[x,y] )

let x be object ; :: thesis: ( x in the carrier of R implies ex y being object st
( y in the carrier of R & S₁[x,y] ) )
assume x in the carrier of R ; :: thesis: ex y being object st
( y in the carrier of R & S₁[x,y] )
then reconsider a = x as Element of R ;
thus ex y being object st
( y in the carrier of R & S₁[x,y] ) :: thesis: verum

proof

take a |^ (Char R) ; :: thesis: ( a |^ (Char R) in the carrier of R & S₁[x,a |^ (Char R)] )
thus ( a |^ (Char R) in the carrier of R & S₁[x,a |^ (Char R)] ) ; :: thesis: verum

end;

end;

consider f being Function of the carrier of R, the carrier of R such that
B: for x being object st x in the carrier of R holds
S₁[x,f . x] from FUNCT_2:sch 1(A);
take f ; :: thesis: for a being Element of R holds f . a = a |^ (Char R)

now :: thesis: for a being Element of R holds f . a = a |^ (Char R)

let a be Element of R; :: thesis: f . a = a |^ (Char R)
S₁[a,f . a] by B;
then consider b being Element of R such that
C: ( a = b & f . b = b |^ (Char R) ) ;
thus f . a = a |^ (Char R) by C; :: thesis: verum

end;

hence for a being Element of R holds f . a = a |^ (Char R) ; :: thesis: verum