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);

.= dom (0_. L) by FUNCT_2:def 1 ;

hence DFT ((0_. L),x,m) = 0_. L by A1, FUNCT_1:2; :: thesis: verum

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 :: thesis: for u being object st u in dom (DFT ((0_. L),x,m)) holds

(DFT ((0_. L),x,m)) . u = (0_. L) . u

dom (DFT ((0_. L),x,m)) =
NAT
by FUNCT_2:def 1
(DFT ((0_. L),x,m)) . u = (0_. L) . u

let u be object ; :: thesis: ( u in dom (DFT ((0_. L),x,m)) implies (DFT ((0_. L),x,m)) . b_{1} = (0_. L) . b_{1} )

assume u in dom (DFT ((0_. L),x,m)) ; :: thesis: (DFT ((0_. L),x,m)) . b_{1} = (0_. L) . b_{1}

then reconsider n = u as Element of NAT by FUNCT_2:def 1;

end;assume u in dom (DFT ((0_. L),x,m)) ; :: thesis: (DFT ((0_. L),x,m)) . b

then reconsider n = u as Element of 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