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

proof

defpred S₁[ Nat] means (modSeq (m,0)) . $1 = 0 ;
let x be object ; :: 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 ;
(modSeq (m,0)) . 0 = m mod 0 by Def1
.= 0 ;
then A2: S₁[ 0 ] ;
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:7; :: thesis: verum

end;

dom (modSeq (m,0)) = NAT by FUNCT_2:def 1;
hence modSeq (m,0) = NAT --> 0 by A1; :: thesis: verum