let n be Nat; :: thesis: for cF being complex-valued XFinSequence
for c being complex number holds c (#) (cF | n) = (c (#) cF) | n
let cF be complex-valued XFinSequence; :: thesis: for c being complex number holds c (#) (cF | n) = (c (#) cF) | n
let c be complex number ; :: thesis: c (#) (cF | n) = (c (#) cF) | n
set ccF = c (#) cF;
set cFn = cF | n;
A2: ( 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 A3: n <= len cF ; :: thesis: c (#) (cF | n) = (c (#) cF) | n

then A4: ( len (cF | n) = n & len ((c (#) cF) | n) = n ) by A2, AFINSQ_1:58;

now

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 A6: i in dom (c (#) (cF | n)) by NAT_1:45;
thus (c (#) (cF | n)) . i = c * ((cF | n) . i) by VALUED_1:6
.= c * (cF . i) by A6, A2, A3, A4, AFINSQ_1:57
.= (c (#) cF) . i by VALUED_1:6
.= ((c (#) cF) | n) . i by A6, A2, A3, A4, AFINSQ_1:57 ; :: thesis: verum

end;

hence c (#) (cF | n) = (c (#) cF) | n by AFINSQ_1:11, A2, A4; :: thesis: verum

end;

suppose n > len cF ; :: thesis: c (#) (cF | n) = (c (#) cF) | n

then ( cF | n = cF & (c (#) cF) | n = c (#) cF ) by AFINSQ_1:56, A2;
hence c (#) (cF | n) = (c (#) cF) | n ; :: thesis: verum

end;

end;