let f be Real_Sequence; :: thesis: f |_ (Seg 0) = seq_const 0
set ff = f |_ (Seg 0);
set g = seq_const 0;
for x being Element of NAT holds (f |_ (Seg 0)) . x = (seq_const 0) . x
proof
let x be Element of NAT ; :: thesis: (f |_ (Seg 0)) . x = (seq_const 0) . x
not x in dom (f | (Seg 0)) ;
hence (f |_ (Seg 0)) . x = (seq_const 0) . x by FUNCT_4:11; :: thesis: verum
end;
hence f |_ (Seg 0) = seq_const 0 by FUNCT_2:63; :: thesis: verum