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

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

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

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

end;

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

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

end;

end;