let n be Nat; :: thesis: for cF being complex-valued XFinSequence
for c being Complex holds c (#) (cF | n) = (c (#) cF) | n
let cF be complex-valued XFinSequence; :: thesis: for c being Complex holds c (#) (cF | n) = (c (#) cF) | n
let c be Complex; :: thesis: c (#) (cF | n) = (c (#) cF) | n
set ccF = c (#) cF;
set cFn = cF | n;
A1: ( len (c (#) cF) = len cF & len (c (#) (cF | n)) = len (cF | n) ) by VALUED_1:def 5;
per cases ( n <= len cF or n > len cF ) ;
suppose A2: n <= len cF ; :: thesis: c (#) (cF | n) = (c (#) cF) | n
then A3: ( len (cF | n) = n & len ((c (#) cF) | n) = n ) by A1, AFINSQ_1:54;
now :: thesis: for i being Nat st i < len (c (#) (cF | n)) holds
(c (#) (cF | n)) . i = ((c (#) cF) | n) . i
let i be Nat; :: thesis: ( i < len (c (#) (cF | n)) implies (c (#) (cF | n)) . i = ((c (#) cF) | n) . i )
assume i < len (c (#) (cF | n)) ; :: thesis: (c (#) (cF | n)) . i = ((c (#) cF) | n) . i
then A4: i in dom (c (#) (cF | n)) by AFINSQ_1:86;
thus (c (#) (cF | n)) . i = c * ((cF | n) . i) by VALUED_1:6
.= c * (cF . i) by A4, A2, AFINSQ_1:53
.= (c (#) cF) . i by VALUED_1:6
.= ((c (#) cF) | n) . i by A4, A1, A2, AFINSQ_1:53 ; :: thesis: verum
end;
hence c (#) (cF | n) = (c (#) cF) | n by A1, A3, AFINSQ_1:9; :: thesis: verum
end;
suppose n > len cF ; :: thesis: c (#) (cF | n) = (c (#) cF) | n
then ( cF | n = cF & (c (#) cF) | n = c (#) cF ) by A1, AFINSQ_1:52;
hence c (#) (cF | n) = (c (#) cF) | n ; :: thesis: verum
end;
end;