for x being set st x in [:A,A:] holds
the multF of M . x in A

proof

let x be set ; :: thesis: ( x in [:A,A:] implies the multF of M . x in A )
assume x in [:A,A:] ; :: thesis: the multF of M . x in A
then consider v, w being object such that
A1: ( v in A & w in A & x = [v,w] ) by ZFMISC_1:def 2;
reconsider v = v, w = w as Element of M by A1;
v * w in A by A1, Def10;
hence the multF of M . x in A by A1, BINOP_1:def 1; :: thesis: verum

end;

then A is Preserv of the multF of M by REALSET1:def 1;
hence the multF of M || A is BinOp of A by REALSET1:2; :: thesis: verum