let f, g be real-valued FinSequence; :: thesis: for m being non zero Nat holds (f ^ g) |^ m = (f |^ m) ^ (g |^ m)
let m be non zero Nat; :: thesis: (f ^ g) |^ m = (f |^ m) ^ (g |^ m)
set ff = (f ^ g) |^ m;
set gg = (f |^ m) ^ (g |^ m);
X1: len ((f ^ g) |^ m) = len (f ^ g) by NAT_3:def 1;
then a1: dom ((f ^ g) |^ m) = dom (f ^ g) by FINSEQ_3:29
.= Seg ((len f) + (len g)) by FINSEQ_1:def 7 ;
a2: ( len (f |^ m) = len f & len (g |^ m) = len g ) by NAT_3:def 1;
dom ((f |^ m) ^ (g |^ m)) = Seg ((len f) + (len g)) by a2, FINSEQ_1:def 7;
then A1: dom ((f ^ g) |^ m) = dom ((f |^ m) ^ (g |^ m)) by a1;
for k being Nat st k in dom ((f ^ g) |^ m) holds
((f ^ g) |^ m) . k = ((f |^ m) ^ (g |^ m)) . k

proof

let k be Nat; :: thesis: ( k in dom ((f ^ g) |^ m) implies ((f ^ g) |^ m) . k = ((f |^ m) ^ (g |^ m)) . k )
len f = len (f |^ m) by NAT_3:def 1;
then X3: dom f = dom (f |^ m) by FINSEQ_3:29;
len g = len (g |^ m) by NAT_3:def 1;
then X4: dom g = dom (g |^ m) by FINSEQ_3:29;
assume B1: k in dom ((f ^ g) |^ m) ; :: thesis: ((f ^ g) |^ m) . k = ((f |^ m) ^ (g |^ m)) . k
then k in dom (f ^ g) by X1, FINSEQ_3:29;

per cases then ( k in dom f or ex n being Nat st
( n in dom g & k = (len f) + n ) ) by FINSEQ_1:25;

suppose X2: k in dom f ; :: thesis: ((f ^ g) |^ m) . k = ((f |^ m) ^ (g |^ m)) . k

((f ^ g) |^ m) . k = ((f ^ g) . k) |^ m by B1, NAT_3:def 1
.= (f . k) |^ m by X2, FINSEQ_1:def 7
.= (f |^ m) . k by X2, X3, NAT_3:def 1
.= ((f |^ m) ^ (g |^ m)) . k by X3, X2, FINSEQ_1:def 7 ;
hence ((f ^ g) |^ m) . k = ((f |^ m) ^ (g |^ m)) . k ; :: thesis: verum

end;

suppose ex n being Nat st
( n in dom g & k = (len f) + n ) ; :: thesis: ((f ^ g) |^ m) . k = ((f |^ m) ^ (g |^ m)) . k

then consider n being Nat such that
O2: ( n in dom g & k = (len f) + n ) ;
X6: k = (len (f |^ m)) + n by O2, a2;
((f ^ g) |^ m) . k = ((f ^ g) . k) |^ m by B1, NAT_3:def 1
.= (g . n) |^ m by O2, FINSEQ_1:def 7
.= (g |^ m) . n by X4, O2, NAT_3:def 1
.= ((f |^ m) ^ (g |^ m)) . k by X6, X4, O2, FINSEQ_1:def 7 ;
hence ((f ^ g) |^ m) . k = ((f |^ m) ^ (g |^ m)) . k ; :: thesis: verum

end;

end;

end;

hence (f ^ g) |^ m = (f |^ m) ^ (g |^ m) by A1, FINSEQ_1:13; :: thesis: verum