let R be 0 -characteristic Ring; :: thesis: Frob R = the carrier of R --> (1. R)
I: Char R = 0 by RING_3:def 6;

now :: thesis: for o being object st o in the carrier of R holds
(Frob R) . o = ( the carrier of R --> (1. R)) . o

let o be object ; :: thesis: ( o in the carrier of R implies (Frob R) . o = ( the carrier of R --> (1. R)) . o )
assume A: o in the carrier of R ; :: thesis: (Frob R) . o = ( the carrier of R --> (1. R)) . o
then reconsider a = o as Element of R ;
thus (Frob R) . o = a |^ 0 by I, defFr
.= 1_ R by BINOM:8
.= ( the carrier of R --> (1. R)) . o by A, FUNCOP_1:7 ; :: thesis: verum

end;

hence Frob R = the carrier of R --> (1. R) ; :: thesis: verum