let n be Nat; :: thesis: for f being n + 1 -element complex-valued XFinSequence holds f = ((f | n) ^ <%0%>) + ((n --> 0) ^ <%(f . n)%>)
let f be n + 1 -element complex-valued XFinSequence; :: thesis: f = ((f | n) ^ <%0%>) + ((n --> 0) ^ <%(f . n)%>)
reconsider g = (f | n) ^ <%0%> as n + 1 -element complex-valued XFinSequence ;
reconsider h = (n --> 0) ^ <%(f . n)%> as n + 1 -element complex-valued XFinSequence ;
A1: dom (g + h) = (n + 1) /\ (n + 1) by CARD_1:def 7;
for i being Nat st i in dom f holds
f . i = (g + h) . i

proof

let i be Nat; :: thesis: ( i in dom f implies f . i = (g + h) . i )
assume B1: i in dom f ; :: thesis: f . i = (g + h) . i

per cases ( i = n or i <> n ) ;

suppose C1: i = n ; :: thesis: f . i = (g + h) . i

i in dom (g + h) by CARD_1:def 7, A1, B1;
then (g + h) . i = (g . i) + (h . i) by VALUED_1:def 1;
hence f . i = (g + h) . i by C1; :: thesis: verum

end;

suppose C1: i <> n ; :: thesis: f . i = (g + h) . i

i in Segm (n + 1) by CARD_1:def 7, B1;
then i < n + 1 by NAT_1:44;
then i <= n by INT_1:7;
then C3: i < n by C1, XXREAL_0:1;
then i in Segm n by NAT_1:44;
then ( i in dom (n --> 0) & i in dom (f | n) ) by CARD_1:def 7;
then C5: (f | n) . i = ((f | n) ^ (f /^ n)) . i by AFINSQ_1:def 3
.= f . i ;
( len (n --> 0) = n & len (f | n) = n ) by CARD_1:def 7;
then ( ((n --> 0) ^ <%(f . n)%>) . i = (n --> 0) . i & ((f | n) ^ <%0%>) . i = (f | n) . i ) by C3, AFINSQ_1:51;
then C6: ( g . i = f . i & h . i = 0 ) by C5;
i in dom (g + h) by CARD_1:def 7, A1, B1;
then (g + h) . i = (g . i) + (h . i) by VALUED_1:def 1;
hence f . i = (g + h) . i by C6; :: thesis: verum

end;

end;

end;

hence f = ((f | n) ^ <%0%>) + ((n --> 0) ^ <%(f . n)%>) by CARD_1:def 7, A1; :: thesis: verum