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

proof

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

proof

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

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

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

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

end;

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

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

end;

end;

end;

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

end;

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