let r be Real; :: thesis: for f, g being real-valued FinSequence holds r |^ (f ^ g) = (r |^ f) ^ (r |^ g)
let f, g be real-valued FinSequence; :: thesis: r |^ (f ^ g) = (r |^ f) ^ (r |^ g)
set fg = f ^ g;
set rf = r |^ f;
set rg = r |^ g;
A1: ( len (f ^ g) = (len f) + (len g) & len ((r |^ f) ^ (r |^ g)) = (len (r |^ f)) + (len (r |^ g)) ) by FINSEQ_1:22;
A2: ( len (r |^ f) = len f & len (r |^ g) = len g & len (r |^ (f ^ g)) = len (f ^ g) ) by CARD_1:def 7;
then A3: ( dom f = dom (r |^ f) & dom g = dom (r |^ g) ) by FINSEQ_3:29;
for i being Nat st 1 <= i & i <= len (f ^ g) holds
(r |^ (f ^ g)) . i = ((r |^ f) ^ (r |^ g)) . i

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len (f ^ g) implies (r |^ (f ^ g)) . i = ((r |^ f) ^ (r |^ g)) . i )
assume ( 1 <= i & i <= len (f ^ g) ) ; :: thesis: (r |^ (f ^ g)) . i = ((r |^ f) ^ (r |^ g)) . i
then A4: i in dom (f ^ g) by FINSEQ_3:25;
then A5: (r |^ (f ^ g)) . i = r to_power ((f ^ g) . i) by Def4;

per cases ( i in dom f or ex j being Nat st
( j in dom g & i = (len f) + j ) ) by A4, FINSEQ_1:25;

suppose A6: i in dom f ; :: thesis: (r |^ (f ^ g)) . i = ((r |^ f) ^ (r |^ g)) . i

then ( (f ^ g) . i = f . i & ((r |^ f) ^ (r |^ g)) . i = (r |^ f) . i ) by A3, FINSEQ_1:def 7;
hence (r |^ (f ^ g)) . i = ((r |^ f) ^ (r |^ g)) . i by A6, Def4, A5; :: thesis: verum

end;

suppose ex j being Nat st
( j in dom g & i = (len f) + j ) ; :: thesis: (r |^ (f ^ g)) . i = ((r |^ f) ^ (r |^ g)) . i

then consider j being Nat such that
A7: ( j in dom g & i = (len f) + j ) ;
( (f ^ g) . i = g . j & ((r |^ f) ^ (r |^ g)) . i = (r |^ g) . j ) by A3, A7, A2, FINSEQ_1:def 7;
hence (r |^ (f ^ g)) . i = ((r |^ f) ^ (r |^ g)) . i by A7, Def4, A5; :: thesis: verum

end;

end;

end;

hence r |^ (f ^ g) = (r |^ f) ^ (r |^ g) by A1, A2; :: thesis: verum