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

proof

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

proof

thus (divSeq 0 ,n) . 0 = 0 div n by Def3
.= 0 ; :: thesis: verum

end;

A3: for x being Nat st S₁[x] holds
S₁[x + 1]

proof

let x be Nat; :: thesis: ( S₁[x] implies S₁[x + 1] )
assume A4: S₁[x] ; :: thesis: S₁[x + 1]

per cases ( x = 0 or 0 <> x ) ;

suppose A5: x = 0 ; :: thesis: S₁[x + 1]

(divSeq 0 ,n) . 1 = n div (0 mod n) by Def3
.= n div 0 ;
hence S₁[x + 1] by A5; :: thesis: verum

end;

suppose 0 <> x ; :: thesis: S₁[x + 1]

hence S₁[x + 1] by A4, Th17, NAT_1:11; :: thesis: verum

end;

end;

end;

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

end;

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