let V, W be non empty right_zeroed ModuleStr over INT.Ring ; :: thesis:
let f be Form of V,W; :: thesis:
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:

hereby :: thesis:

assume A3: f is constant ; :: thesis:
let v be Vector of V; :: thesis:
let w be Vector of W; :: thesis:

per cases by A2;

suppose A4: f is additiveFAF ; :: thesis:

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

end;

suppose A5: f is additiveSAF ; :: thesis:

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

end;

end;

end;

hereby :: thesis:

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

now :: thesis:

let x, y be object ; :: thesis:
assume that
A7: x in dom f and
A8: y in dom f ; :: thesis:
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 by A6
.= f . (s,t) by A6
.= f . y by A10 ; :: thesis:

end;

hence f is constant ; :: thesis:

end;