let s, m be Nat; :: thesis: for f being s -element natural-valued positive-yielding FinSequence st s = 2 |^ m & f = s |-> 2 holds
f is m -solution_of_Sierp167
let f be s -element natural-valued positive-yielding FinSequence; :: thesis: ( s = 2 |^ m & f = s |-> 2 implies f is m -solution_of_Sierp167 )
assume A1: ( s = 2 |^ m & f = s |-> 2 ) ; :: thesis: f is m -solution_of_Sierp167
set r = (2 |^ m) " ;
W3: dom f = Seg s by FINSEQ_1:89;
W2: dom ((f | s) ") = Seg s by W3, VALUED_1:def 7;
len f = s by CARD_1:def 7;
then ST: f | s = f ;
f0: len (((f | s) ") |^ m) = len ((f | s) ") by NAT_3:def 1;
then f1: dom (((f | s) ") |^ m) = Seg s by W2, FINSEQ_3:29;
then F1: dom (((f | s) ") |^ m) = dom (s |-> ((2 |^ m) ")) ;
for x being object st x in dom (((f | s) ") |^ m) holds
(((f | s) ") |^ m) . x = (s |-> ((2 |^ m) ")) . x

proof

let x be object ; :: thesis: ( x in dom (((f | s) ") |^ m) implies (((f | s) ") |^ m) . x = (s |-> ((2 |^ m) ")) . x )
assume H1: x in dom (((f | s) ") |^ m) ; :: thesis: (((f | s) ") |^ m) . x = (s |-> ((2 |^ m) ")) . x
then f2: x in dom ((f | s) ") by f0, FINSEQ_3:29;
then reconsider i = x as Nat ;
H2: i in Seg s by H1, f1;
CC: ((f | s) ") . i = ((f | s) . i) " by f2, VALUED_1:def 7
.= 2 " by A1, H2, FUNCOP_1:7 ;
(((f | s) ") |^ m) . x = (1 / 2) to_power m by CC, H1, NAT_3:def 1
.= (1 to_power m) / (2 to_power m) by POWER:31
.= (s |-> ((2 |^ m) ")) . x by H2, FUNCOP_1:7 ;
hence (((f | s) ") |^ m) . x = (s |-> ((2 |^ m) ")) . x ; :: thesis: verum

end;

then Z2: ((f | s) ") |^ m = s |-> ((2 |^ m) ") by F1, FUNCT_1:2;
Sum (s |-> ((2 |^ m) ")) = s * ((2 |^ m) ") by RVSUM_1:80
.= 1 by A1, XCMPLX_0:def 7 ;
hence f is m -solution_of_Sierp167 by Z2, ST; :: thesis: verum