now :: thesis: for b being Element of Bags n holds |.(0_ (n,F_Real)).| . b = (0_ (n,F_Real)) . b

let b be Element of Bags n; :: thesis: |.(0_ (n,F_Real)).| . b = (0_ (n,F_Real)) . b
thus |.(0_ (n,F_Real)).| . b = |.((0_ (n,F_Real)) . b).| by Def1
.= (0_ (n,F_Real)) . b ; :: thesis: verum

end;

hence |.(0_ (n,F_Real)).| = 0_ (n,F_Real) ; :: thesis: verum