let rf1, rf2 be real-valued FinSequence; :: thesis:
set rf12 = rf1 ^ rf2;
set s12 = sqrt (rf1 ^ rf2);
set s1 = sqrt rf1;
set s2 = sqrt rf2;
A1: dom (sqrt (rf1 ^ rf2)) = dom (rf1 ^ rf2) by PARTFUN3:def 5;
A2: dom (sqrt rf2) = dom rf2 by PARTFUN3:def 5;
then A3: len (sqrt rf2) = len rf2 by FINSEQ_3:29;
A4: dom (sqrt rf1) = dom rf1 by PARTFUN3:def 5;
then A5: len (sqrt rf1) = len rf1 by FINSEQ_3:29;
A6: for n being Nat st 1 <= n & n <= len (sqrt (rf1 ^ rf2)) holds
(sqrt (rf1 ^ rf2)) . n = ((sqrt rf1) ^ (sqrt rf2)) . n

proof

let n be Nat; :: thesis:
assume ( 1 <= n & n <= len (sqrt (rf1 ^ rf2)) ) ; :: thesis:
then A7: n in dom (sqrt (rf1 ^ rf2)) by FINSEQ_3:25;
then A8: (sqrt (rf1 ^ rf2)) . n = sqrt ((rf1 ^ rf2) . n) by PARTFUN3:def 5;

per cases by A1, A7, FINSEQ_1:25;

suppose A9: n in dom rf1 ; :: thesis:

then ( (rf1 ^ rf2) . n = rf1 . n & (sqrt rf1) . n = sqrt (rf1 . n) ) by A4, FINSEQ_1:def 7, PARTFUN3:def 5;
hence (sqrt (rf1 ^ rf2)) . n = ((sqrt rf1) ^ (sqrt rf2)) . n by A4, A8, A9, FINSEQ_1:def 7; :: thesis:

end;

suppose ex m being Nat st
( m in dom rf2 & n = (len rf1) + m ) ; :: thesis:

then consider m being Nat such that
A10: ( m in dom rf2 & n = (len rf1) + m ) ;
( (rf1 ^ rf2) . n = rf2 . m & (sqrt rf2) . m = sqrt (rf2 . m) ) by A2, A10, FINSEQ_1:def 7, PARTFUN3:def 5;
hence (sqrt (rf1 ^ rf2)) . n = ((sqrt rf1) ^ (sqrt rf2)) . n by A2, A5, A8, A10, FINSEQ_1:def 7; :: thesis:

end;

end;

end;

len (sqrt (rf1 ^ rf2)) = len (rf1 ^ rf2) by A1, FINSEQ_3:29;
then len (sqrt (rf1 ^ rf2)) = (len (sqrt rf1)) + (len (sqrt rf2)) by A5, A3, FINSEQ_1:22;
then len (sqrt (rf1 ^ rf2)) = len ((sqrt rf1) ^ (sqrt rf2)) by FINSEQ_1:22;
hence sqrt (rf1 ^ rf2) = (sqrt rf1) ^ (sqrt rf2) by A6; :: thesis: