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

proof

let x be set ; :: 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 ;
defpred S₁[ Nat] means (divSeq m,0 ) . $1 = 0 ;
A2: S₁[ 0 ]

proof

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

end;

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

proof

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

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

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

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

end;

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

hence S₁[n + 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 m,0 ) . x = 0 ;
hence (divSeq m,0 ) . x = (NAT --> 0 ) . x by FUNCOP_1:13; :: thesis: verum

end;

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