let f be complex-valued XFinSequence; :: thesis: Sequel f = f ^ (seq_const 0)
A1: dom (Sequel f) = dom (f ^ (seq_const 0))

proof

dom (Sequel f) = (dom (NAT --> 0)) \/ (dom f) by FUNCT_4:def 1
.= NAT \/ (dom f)
.= dom (f ^ (seq_const 0)) by COMSEQ_1:1 ;
hence dom (Sequel f) = dom (f ^ (seq_const 0)) ; :: thesis: verum

end;

for x being Nat holds (Sequel f) . x = (f ^ (seq_const 0)) . x

proof

let x be Nat; :: thesis: (Sequel f) . x = (f ^ (seq_const 0)) . x
( (Sequel f) . x = f . x & (f ^ (seq_const 0)) . x = f . x ) by SCX, SFX;
hence (Sequel f) . x = (f ^ (seq_const 0)) . x ; :: thesis: verum

end;

hence Sequel f = f ^ (seq_const 0) by A1; :: thesis: verum