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 ;
reconsider v1 = v as BilinearOperator of X,Y,Z by ;
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
.= (L . (x1,y)) + (L . (x2,y)) by ;
:: 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 ;
:: 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
.= (L . (x,y1)) + (L . (x,y2)) by ;
:: 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 ;
:: thesis: verum
end;
hence v + u is BilinearOperator of X,Y,Z by ; :: 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 ;
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
.= (L . (x1,y)) + (L . (x2,y)) by ;
:: 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 ;
:: 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
.= (L . (x,y1)) + (L . (x,y2)) by ;
:: 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 ;
:: thesis: verum
end;
hence b * v is BilinearOperator of X,Y,Z by ; :: 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 ; :: thesis: verum