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 = 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 the Element of A ; :: thesis: <*a9*> /. i = aR * the Element of A
dom <*a9*> = {1} by FINSEQ_1:2, FINSEQ_1:38;
then A2: i = 1 by A1, TARSKI:def 1;
thus <*a9*> /. i = <*a9*> . i by A1, PARTFUN1:def 6
.= aR * the Element of A by A2 ; :: thesis: verum