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

proof

defpred S₁[ Nat] means (divSeq (0,n)) . $1 = 0 ;
let x be object ; :: 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 ;
A2: for x being Nat st S₁[x] holds
S₁[x + 1]

proof

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

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

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

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

end;

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

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

end;

end;

end;

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

end;

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