set n = Char R;
let g1, g2 be Function of R,R; :: thesis: ( ( for a being Element of R holds g1 . a = a |^ (Char R) ) & ( for a being Element of R holds g2 . a = a |^ (Char R) ) implies g1 = g2 )
assume that
A1: for a being Element of R holds g1 . a = a |^ (Char R) and
A2: for a being Element of R holds g2 . a = a |^ (Char R) ; :: thesis: g1 = g2

now :: thesis: for x being object st x in the carrier of R holds
g1 . x = g2 . x

let x be object ; :: thesis: ( x in the carrier of R implies g1 . x = g2 . x )
assume x in the carrier of R ; :: thesis: g1 . x = g2 . x
then reconsider a = x as Element of R ;
thus g1 . x = a |^ (Char R) by A1
.= g2 . x by A2 ; :: thesis: verum

end;

hence g1 = g2 ; :: thesis: verum