consider a being Element of A;
reconsider aR = a as Element of R ;
reconsider a9 = a * a as Element of R ;
set p = <*a9*>;
take <*a9*> ; :: thesis: for i being set st i in dom <*a9*> holds
ex u being Element of R ex a being Element of A st <*a9*> /. i = u * a
let i be set ; :: thesis: ( i in dom <*a9*> implies ex u being Element of R ex a being Element of A st <*a9*> /. i = u * a )
assume A1: i in dom <*a9*> ; :: thesis: ex u being Element of R ex a being Element of A st <*a9*> /. i = u * a
take aR ; :: thesis: ex a being Element of A st <*a9*> /. i = aR * a
take a ; :: thesis: <*a9*> /. i = aR * a
dom <*a9*> = {1} by FINSEQ_1:4, FINSEQ_1:55;
then A2: i = 1 by A1, TARSKI:def 1;
thus <*a9*> /. i = <*a9*> . i by A1, PARTFUN1:def 8
.= aR * a by A2, FINSEQ_1:57 ; :: thesis: verum