let R be ZeroStr ; :: thesis: <*> the carrier of R is trivial
set f = <*> the carrier of R;
for i being object st i in dom (<*> the carrier of R) holds
(<*> the carrier of R) . i = 0. R ;
hence <*> the carrier of R is trivial by REALALG2:def 4; :: thesis: verum