let K be non empty right_complementable add-associative right_zeroed doubleLoopStr ; :: thesis: for V, W being non empty right_zeroed ModuleStr over K
for f being Form of V,W st ( f is additiveFAF or f is additiveSAF ) holds
( f is constant iff for v being Vector of V
for w being Vector of W holds f . (v,w) = 0. K )
let V, W be non empty right_zeroed ModuleStr over K; :: thesis: for f being Form of V,W st ( f is additiveFAF or f is additiveSAF ) holds
( f is constant iff for v being Vector of V
for w being Vector of W holds f . (v,w) = 0. K )
let f be Form of V,W; :: thesis: ( ( f is additiveFAF or f is additiveSAF ) implies ( f is constant iff for v being Vector of V
for w being Vector of W holds f . (v,w) = 0. K ) )
A1: dom f = [: the carrier of V, the carrier of W:] by FUNCT_2:def 1;
assume A2: ( f is additiveFAF or f is additiveSAF ) ; :: thesis: ( f is constant iff for v being Vector of V
for w being Vector of W holds f . (v,w) = 0. K )

hereby :: thesis: ( ( for v being Vector of V
for w being Vector of W holds f . (v,w) = 0. K ) implies f is constant )

assume A3: f is constant ; :: thesis: for v being Vector of V
for w being Vector of W holds f . (b₃,b₄) = 0. K
let v be Vector of V; :: thesis: for w being Vector of W holds f . (b₂,b₃) = 0. K
let w be Vector of W; :: thesis: f . (b₁,b₂) = 0. K

per cases ( f is additiveFAF or f is additiveSAF ) by A2;

suppose A4: f is additiveFAF ; :: thesis: f . (b₁,b₂) = 0. K

thus f . (v,w) = f . (v,(0. W)) by A1, A3, BINOP_1:19
.= 0. K by A4, Th29 ; :: thesis: verum

end;

suppose A5: f is additiveSAF ; :: thesis: f . (b₁,b₂) = 0. K

thus f . (v,w) = f . ((0. V),w) by A1, A3, BINOP_1:19
.= 0. K by A5, Th30 ; :: thesis: verum

end;

end;

end;

hereby :: thesis: verum

assume A6: for v being Vector of V
for w being Vector of W holds f . (v,w) = 0. K ; :: thesis: f is constant

now :: thesis: for x, y being object st x in dom f & y in dom f holds
f . x = f . y

let x, y be object ; :: thesis: ( x in dom f & y in dom f implies f . x = f . y )
assume that
A7: x in dom f and
A8: y in dom f ; :: thesis: f . x = f . y
consider v being Vector of V, w being Vector of W such that
A9: x = [v,w] by A7, DOMAIN_1:1;
consider s being Vector of V, t being Vector of W such that
A10: y = [s,t] by A8, DOMAIN_1:1;
thus f . x = f . (v,w) by A9
.= 0. K by A6
.= f . (s,t) by A6
.= f . y by A10 ; :: thesis: verum

end;

hence f is constant by FUNCT_1:def 10; :: thesis: verum

end;