set f = seq_id Zeroseq;
let n be object ; :: thesis: (seq_id Zeroseq) . n = 0

per cases ( n in dom (seq_id Zeroseq) or not n in dom (seq_id Zeroseq) ) ;

suppose A1: n in dom (seq_id Zeroseq) ; :: thesis: (seq_id Zeroseq) . n = 0

dom (seq_id Zeroseq) = NAT by FUNCT_2:def 1;
hence (seq_id Zeroseq) . n = 0 by A1, FUNCOP_1:7; :: thesis: verum

end;

suppose not n in dom (seq_id Zeroseq) ; :: thesis: (seq_id Zeroseq) . n = 0

hence (seq_id Zeroseq) . n = 0 by FUNCT_1:def 2; :: thesis: verum

end;

end;