set a = the Element of A;
reconsider aR = the Element of A as Element of R ;
reconsider a9 = the Element of A * the Element of 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 = a * u
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 = a * u )
assume A3: i in dom <*a9*> ; :: thesis: ex u being Element of R ex a being Element of A st <*a9*> /. i = a * u
take aR ; :: thesis: ex a being Element of A st <*a9*> /. i = a * aR
take the Element of A ; :: thesis: <*a9*> /. i = the Element of A * aR
dom <*a9*> = {1} by FINSEQ_1:2, FINSEQ_1:38;
then A4: i = 1 by A3, TARSKI:def 1;
thus <*a9*> /. i = <*a9*> . i by A3, PARTFUN1:def 6
.= the Element of A * aR by A4, FINSEQ_1:40 ; :: thesis: verum