let m be Nat; :: thesis: modSeq m,0 = NAT --> 0
set fm = modSeq m,0 ;
A1: dom (modSeq m,0 ) = NAT by FUNCT_2:def 1;
for x being set st x in dom (modSeq m,0 ) holds
(modSeq m,0 ) . x = (NAT --> 0 ) . x

proof

let x be set ; :: thesis: ( x in dom (modSeq m,0 ) implies (modSeq m,0 ) . x = (NAT --> 0 ) . x )
assume x in dom (modSeq m,0 ) ; :: thesis: (modSeq m,0 ) . x = (NAT --> 0 ) . x
then reconsider x = x as Element of NAT ;
defpred S₁[ Nat] means (modSeq m,0 ) . $1 = 0 ;
A2: S₁[ 0 ]

proof

(modSeq m,0 ) . 0 = m mod 0 by Def2
.= 0 ;
hence S₁[ 0 ] ; :: thesis: verum

end;

A3: for n being Nat st S₁[n] holds
S₁[n + 1] by Th14, NAT_1:11;
for n being Nat holds S₁[n] from NAT_1:sch 2(A2, A3);
then (modSeq m,0 ) . x = 0 ;
hence (modSeq m,0 ) . x = (NAT --> 0 ) . x by FUNCOP_1:13; :: thesis: verum

end;

hence modSeq m,0 = NAT --> 0 by A1, Lm5, FUNCT_1:9; :: thesis: verum