let r be Real; :: thesis: sqrt <*r*> = <*(sqrt r)*>
set R = <*r*>;
A1: <*r*> . 1 = r by FINSEQ_1:40;
A2: dom <*r*> = dom (sqrt <*r*>) by PARTFUN3:def 5;
then A3: len <*r*> = len (sqrt <*r*>) by FINSEQ_3:29;
( 1 in Seg 1 & dom <*r*> = Seg 1 ) by FINSEQ_1:38;
then ( len <*r*> = 1 & (sqrt <*r*>) . 1 = sqrt r ) by A2, A1, FINSEQ_1:40, PARTFUN3:def 5;
hence sqrt <*r*> = <*(sqrt r)*> by A3, FINSEQ_1:40; :: thesis: verum