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 )

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 )

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_{3},b_{4}) = 0. K

let v be Vector of V; :: thesis: for w being Vector of W holds f . (b_{2},b_{3}) = 0. K

let w be Vector of W; :: thesis: f . (b_{1},b_{2}) = 0. K

end;for w being Vector of W holds f . (b

let v be Vector of V; :: thesis: for w being Vector of W holds f . (b

let w be Vector of W; :: thesis: f . (b

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

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

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

hence
f is constant
by FUNCT_1:def 10; :: thesis: verumf . 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;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