let m be Nat; 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 ; for x being Element of L holds DFT ((0_. L),x,m) = 0_. L
let x be Element of L; DFT ((0_. L),x,m) = 0_. L
set q = DFT ((0_. L),x,m);
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; verum