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

proof

defpred S₁[ Nat] means (modSeq 0 ,n) . $1 = 0 ;
let x be set ; :: thesis: ( x in dom (modSeq 0 ,n) implies (modSeq 0 ,n) . x = (NAT --> 0 ) . x )
assume x in dom (modSeq 0 ,n) ; :: thesis: (modSeq 0 ,n) . x = (NAT --> 0 ) . x
then reconsider x = x as Element of NAT ;
(modSeq 0 ,n) . 0 = 0 mod n by Def2
.= 0 ;
then A2: S₁[ 0 ] ;
A3: for x being Nat st S₁[x] holds
S₁[x + 1] by Th14, NAT_1:11;
for n being Nat holds S₁[n] from NAT_1:sch 2(A2, A3);
then (modSeq 0 ,n) . x = 0 ;
hence (modSeq 0 ,n) . x = (NAT --> 0 ) . x by FUNCOP_1:13; :: thesis: verum

end;

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