let K be non empty right_complementable add-associative right_zeroed doubleLoopStr ; :: thesis: for V, W being non empty right_zeroed VectSpStr of 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 VectSpStr of 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 ) )
assume A1: ( 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 )
A2: dom f = [:the carrier of V,the carrier of W:] by FUNCT_2:def 1;

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

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

thus f . v,w = f . v,(0. W) by A2, A3, BINOP_1:31
.= 0. K by A4, Th30 ; :: thesis: verum

end;

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

thus f . v,w = f . (0. V),w by A2, A3, BINOP_1:31
.= 0. K by A5, Th31 ; :: 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

let x, y be set ; :: 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:9;
consider s being Vector of V, t being Vector of W such that
A10: y = [s,t] by A8, DOMAIN_1:9;
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 16; :: thesis: verum

end;