let X, Y, Z be RealLinearSpace; :: thesis: BilinearOperators (X,Y,Z) is linearly-closed
set W = BilinearOperators (X,Y,Z);
A1: for v, u being VECTOR of (RealVectSpace ( the carrier of [:X,Y:],Z)) st v in BilinearOperators (X,Y,Z) & u in BilinearOperators (X,Y,Z) holds
v + u in BilinearOperators (X,Y,Z)

proof

let v, u be VECTOR of (RealVectSpace ( the carrier of [:X,Y:],Z)); :: thesis: ( v in BilinearOperators (X,Y,Z) & u in BilinearOperators (X,Y,Z) implies v + u in BilinearOperators (X,Y,Z) )
assume that
A2: v in BilinearOperators (X,Y,Z) and
A3: u in BilinearOperators (X,Y,Z) ; :: thesis: v + u in BilinearOperators (X,Y,Z)
reconsider u1 = u as BilinearOperator of X,Y,Z by A3, Def6;
reconsider v1 = v as BilinearOperator of X,Y,Z by A2, Def6;
v + u is BilinearOperator of X,Y,Z

proof

reconsider L = v + u as Function of [:X,Y:],Z by FUNCT_2:66;
A4: for x1, x2 being Point of X
for y being Point of Y holds L . ((x1 + x2),y) = (L . (x1,y)) + (L . (x2,y))

proof

let x1, x2 be Point of X; :: thesis: for y being Point of Y holds L . ((x1 + x2),y) = (L . (x1,y)) + (L . (x2,y))
let y be Point of Y; :: thesis: L . ((x1 + x2),y) = (L . (x1,y)) + (L . (x2,y))
A5: ( [x1,y] is Element of [:X,Y:] & [x2,y] is Element of [:X,Y:] & [(x1 + x2),y] is Element of [:X,Y:] ) ;
hence L . ((x1 + x2),y) = (v1 . ((x1 + x2),y)) + (u1 . ((x1 + x2),y)) by LOPBAN_1:1
.= ((v1 . (x1,y)) + (v1 . (x2,y))) + (u1 . ((x1 + x2),y)) by LOPBAN_8:11
.= ((v1 . (x1,y)) + (v1 . (x2,y))) + ((u1 . (x1,y)) + (u1 . (x2,y))) by LOPBAN_8:11
.= ((v1 . (x1,y)) + (u1 . (x1,y))) + ((v1 . (x2,y)) + (u1 . (x2,y))) by LM14
.= (L . (x1,y)) + ((v1 . (x2,y)) + (u1 . (x2,y))) by A5, LOPBAN_1:1
.= (L . (x1,y)) + (L . (x2,y)) by A5, LOPBAN_1:1 ;
:: thesis: verum

end;

A6: for x being Point of X
for y being Point of Y
for a being Real holds L . ((a * x),y) = a * (L . (x,y))

proof

let x be Point of X; :: thesis: for y being Point of Y
for a being Real holds L . ((a * x),y) = a * (L . (x,y))
let y be Point of Y; :: thesis: for a being Real holds L . ((a * x),y) = a * (L . (x,y))
let a be Real; :: thesis: L . ((a * x),y) = a * (L . (x,y))
A7: ( [x,y] is Element of [:X,Y:] & [(a * x),y] is Element of [:X,Y:] ) ;
hence L . ((a * x),y) = (v1 . ((a * x),y)) + (u1 . ((a * x),y)) by LOPBAN_1:1
.= (a * (v1 . (x,y))) + (u1 . ((a * x),y)) by LOPBAN_8:11
.= (a * (v1 . (x,y))) + (a * (u1 . (x,y))) by LOPBAN_8:11
.= a * ((v1 . (x,y)) + (u1 . (x,y))) by RLVECT_1:def 5
.= a * (L . (x,y)) by A7, LOPBAN_1:1 ;
:: thesis: verum

end;

A8: for x being Point of X
for y1, y2 being Point of Y holds L . (x,(y1 + y2)) = (L . (x,y1)) + (L . (x,y2))

proof

let x be Point of X; :: thesis: for y1, y2 being Point of Y holds L . (x,(y1 + y2)) = (L . (x,y1)) + (L . (x,y2))
let y1, y2 be Point of Y; :: thesis: L . (x,(y1 + y2)) = (L . (x,y1)) + (L . (x,y2))
A9: ( [x,y1] is Element of [:X,Y:] & [x,y2] is Element of [:X,Y:] & [x,(y1 + y2)] is Element of [:X,Y:] ) ;
hence L . (x,(y1 + y2)) = (v1 . (x,(y1 + y2))) + (u1 . (x,(y1 + y2))) by LOPBAN_1:1
.= ((v1 . (x,y1)) + (v1 . (x,y2))) + (u1 . (x,(y1 + y2))) by LOPBAN_8:11
.= ((v1 . (x,y1)) + (v1 . (x,y2))) + ((u1 . (x,y1)) + (u1 . (x,y2))) by LOPBAN_8:11
.= ((v1 . (x,y1)) + (u1 . (x,y1))) + ((v1 . (x,y2)) + (u1 . (x,y2))) by LM14
.= (L . (x,y1)) + ((v1 . (x,y2)) + (u1 . (x,y2))) by A9, LOPBAN_1:1
.= (L . (x,y1)) + (L . (x,y2)) by A9, LOPBAN_1:1 ;
:: thesis: verum

end;

for x being Point of X
for y being Point of Y
for a being Real holds L . (x,(a * y)) = a * (L . (x,y))

proof

let x be Point of X; :: thesis: for y being Point of Y
for a being Real holds L . (x,(a * y)) = a * (L . (x,y))
let y be Point of Y; :: thesis: for a being Real holds L . (x,(a * y)) = a * (L . (x,y))
let a be Real; :: thesis: L . (x,(a * y)) = a * (L . (x,y))
A10: ( [x,y] is Element of [:X,Y:] & [x,(a * y)] is Element of [:X,Y:] ) ;
hence L . (x,(a * y)) = (v1 . (x,(a * y))) + (u1 . (x,(a * y))) by LOPBAN_1:1
.= (a * (v1 . (x,y))) + (u1 . (x,(a * y))) by LOPBAN_8:11
.= (a * (v1 . (x,y))) + (a * (u1 . (x,y))) by LOPBAN_8:11
.= a * ((v1 . (x,y)) + (u1 . (x,y))) by RLVECT_1:def 5
.= a * (L . (x,y)) by A10, LOPBAN_1:1 ;
:: thesis: verum

end;

hence v + u is BilinearOperator of X,Y,Z by A4, A6, A8, LOPBAN_8:11; :: thesis: verum

end;

hence v + u in BilinearOperators (X,Y,Z) by Def6; :: thesis: verum

end;

for b being Real
for v being VECTOR of (RealVectSpace ( the carrier of [:X,Y:],Z)) st v in BilinearOperators (X,Y,Z) holds
b * v in BilinearOperators (X,Y,Z)

proof

let b be Real; :: thesis: for v being VECTOR of (RealVectSpace ( the carrier of [:X,Y:],Z)) st v in BilinearOperators (X,Y,Z) holds
b * v in BilinearOperators (X,Y,Z)
let v be VECTOR of (RealVectSpace ( the carrier of [:X,Y:],Z)); :: thesis: ( v in BilinearOperators (X,Y,Z) implies b * v in BilinearOperators (X,Y,Z) )
assume A11: v in BilinearOperators (X,Y,Z) ; :: thesis: b * v in BilinearOperators (X,Y,Z)
reconsider v1 = v as BilinearOperator of X,Y,Z by A11, Def6;
b * v is BilinearOperator of X,Y,Z

proof

reconsider L = b * v as Function of [:X,Y:],Z by FUNCT_2:66;
A12: for x1, x2 being Point of X
for y being Point of Y holds L . ((x1 + x2),y) = (L . (x1,y)) + (L . (x2,y))

proof

let x1, x2 be Point of X; :: thesis: for y being Point of Y holds L . ((x1 + x2),y) = (L . (x1,y)) + (L . (x2,y))
let y be Point of Y; :: thesis: L . ((x1 + x2),y) = (L . (x1,y)) + (L . (x2,y))
A13: ( [x1,y] is Element of [:X,Y:] & [x2,y] is Element of [:X,Y:] & [(x1 + x2),y] is Element of [:X,Y:] ) ;
hence L . ((x1 + x2),y) = b * (v1 . ((x1 + x2),y)) by LOPBAN_1:2
.= b * ((v1 . (x1,y)) + (v1 . (x2,y))) by LOPBAN_8:11
.= (b * (v1 . (x1,y))) + (b * (v1 . (x2,y))) by RLVECT_1:def 5
.= (L . (x1,y)) + (b * (v1 . (x2,y))) by A13, LOPBAN_1:2
.= (L . (x1,y)) + (L . (x2,y)) by A13, LOPBAN_1:2 ;
:: thesis: verum

end;

A14: for x being Point of X
for y being Point of Y
for a being Real holds L . ((a * x),y) = a * (L . (x,y))

proof

let x be Point of X; :: thesis: for y being Point of Y
for a being Real holds L . ((a * x),y) = a * (L . (x,y))
let y be Point of Y; :: thesis: for a being Real holds L . ((a * x),y) = a * (L . (x,y))
let a be Real; :: thesis: L . ((a * x),y) = a * (L . (x,y))
A15: ( [x,y] is Element of [:X,Y:] & [(a * x),y] is Element of [:X,Y:] ) ;
hence L . ((a * x),y) = b * (v1 . ((a * x),y)) by LOPBAN_1:2
.= b * (a * (v1 . (x,y))) by LOPBAN_8:11
.= (b * a) * (v1 . (x,y)) by RLVECT_1:def 7
.= a * (b * (v1 . (x,y))) by RLVECT_1:def 7
.= a * (L . (x,y)) by A15, LOPBAN_1:2 ;
:: thesis: verum

end;

A16: for x being Point of X
for y1, y2 being Point of Y holds L . (x,(y1 + y2)) = (L . (x,y1)) + (L . (x,y2))

proof

let x be Point of X; :: thesis: for y1, y2 being Point of Y holds L . (x,(y1 + y2)) = (L . (x,y1)) + (L . (x,y2))
let y1, y2 be Point of Y; :: thesis: L . (x,(y1 + y2)) = (L . (x,y1)) + (L . (x,y2))
A17: ( [x,y1] is Element of [:X,Y:] & [x,y2] is Element of [:X,Y:] & [x,(y1 + y2)] is Element of [:X,Y:] ) ;
hence L . (x,(y1 + y2)) = b * (v1 . (x,(y1 + y2))) by LOPBAN_1:2
.= b * ((v1 . (x,y1)) + (v1 . (x,y2))) by LOPBAN_8:11
.= (b * (v1 . (x,y1))) + (b * (v1 . (x,y2))) by RLVECT_1:def 5
.= (L . (x,y1)) + (b * (v1 . (x,y2))) by A17, LOPBAN_1:2
.= (L . (x,y1)) + (L . (x,y2)) by A17, LOPBAN_1:2 ;
:: thesis: verum

end;

for x being Point of X
for y being Point of Y
for a being Real holds L . (x,(a * y)) = a * (L . (x,y))

proof

let x be Point of X; :: thesis: for y being Point of Y
for a being Real holds L . (x,(a * y)) = a * (L . (x,y))
let y be Point of Y; :: thesis: for a being Real holds L . (x,(a * y)) = a * (L . (x,y))
let a be Real; :: thesis: L . (x,(a * y)) = a * (L . (x,y))
A18: ( [x,y] is Element of [:X,Y:] & [x,(a * y)] is Element of [:X,Y:] ) ;
hence L . (x,(a * y)) = b * (v1 . (x,(a * y))) by LOPBAN_1:2
.= b * (a * (v1 . (x,y))) by LOPBAN_8:11
.= (b * a) * (v1 . (x,y)) by RLVECT_1:def 7
.= a * (b * (v1 . (x,y))) by RLVECT_1:def 7
.= a * (L . (x,y)) by A18, LOPBAN_1:2 ;
:: thesis: verum

end;

hence b * v is BilinearOperator of X,Y,Z by A12, A14, A16, LOPBAN_8:11; :: thesis: verum

end;

hence b * v in BilinearOperators (X,Y,Z) by Def6; :: thesis: verum

end;

hence BilinearOperators (X,Y,Z) is linearly-closed by A1, RLSUB_1:def 1; :: thesis: verum