let rf be real-valued FinSequence; :: thesis: sqrt (rf ^2) = abs rf
set F = rf ^2 ;
set S = sqrt (rf ^2);
A1: dom (sqrt (rf ^2)) = dom (rf ^2) by PARTFUN3:def 5;
A2: ( dom (abs rf) = dom rf & dom (rf ^2) = dom rf ) by VALUED_1:11, VALUED_1:def 11;
now :: thesis: for x being object st x in dom (abs rf) holds
(abs rf) . x = (sqrt (rf ^2)) . x
let x be object ; :: thesis: ( x in dom (abs rf) implies (abs rf) . x = (sqrt (rf ^2)) . x )
reconsider fx = rf . x as Real ;
A3: ( fx >= 0 or fx < 0 ) ;
assume A4: x in dom (abs rf) ; :: thesis: (abs rf) . x = (sqrt (rf ^2)) . x
then ( (rf ^2) . x = fx ^2 & (sqrt (rf ^2)) . x = sqrt ((rf ^2) . x) ) by A2, A1, PARTFUN3:def 5, VALUED_1:11;
then A5: ( ( (sqrt (rf ^2)) . x = fx & fx >= 0 ) or ( (sqrt (rf ^2)) . x = - fx & fx < 0 ) ) by A3, SQUARE_1:22, SQUARE_1:23;
(abs rf) . x = |.fx.| by A4, VALUED_1:def 11;
hence (abs rf) . x = (sqrt (rf ^2)) . x by A5, ABSVALUE:def 1; :: thesis: verum
end;
hence sqrt (rf ^2) = abs rf by A2, A1, FUNCT_1:2; :: thesis: verum