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:17
.= (0_. L) . n by FUNCOP_1:7
.= (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:7
.= (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:2; :: thesis: verum