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