let m be Nat; :: thesis: for L being non empty well-unital doubleLoopStr
for x being Element of L holds DFT (0_. L),x,m = 0_. L
let L be non empty well-unital doubleLoopStr ; :: thesis: for x being Element of L holds DFT (0_. L),x,m = 0_. L
let x be Element of L; :: thesis: DFT (0_. L),x,m = 0_. L
set q = DFT (0_. L),x,m;

A1: now

let u be set ; :: thesis: ( u in dom (DFT (0_. L),x,m) implies (DFT (0_. L),x,m) . b₁ = (0_. L) . b₁ )
assume u in dom (DFT (0_. L),x,m) ; :: thesis: (DFT (0_. L),x,m) . b₁ = (0_. L) . b₁
then reconsider n = u as Element of NAT by FUNCT_2:def 1;

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

suppose n < m ; :: thesis: (DFT (0_. L),x,m) . b₁ = (0_. L) . b₁

hence (DFT (0_. L),x,m) . u = eval (0_. L),(x |^ n) by Def7
.= 0. L by POLYNOM4:20
.= (0_. L) . n by FUNCOP_1:13
.= (0_. L) . u ;
:: thesis: verum

end;

suppose n >= m ; :: thesis: (DFT (0_. L),x,m) . b₁ = (0_. L) . b₁

hence (DFT (0_. L),x,m) . u = 0. L by Def7
.= (0_. L) . n by FUNCOP_1:13
.= (0_. L) . u ;
:: thesis: verum

end;

end;

end;

dom (DFT (0_. L),x,m) = NAT by FUNCT_2:def 1
.= dom (0_. L) by FUNCT_2:def 1 ;
hence DFT (0_. L),x,m = 0_. L by A1, FUNCT_1:9; :: thesis: verum