let X be RealLinearSpace-Sequence; for Y being RealLinearSpace ex I being Function of [:(product X),Y:],(product (X ^ <*Y*>)) st
( I is one-to-one & I is onto & ( for x being Point of (product X)
for y being Point of Y ex x1, y1 being FinSequence st
( x = x1 & <*y*> = y1 & I . (x,y) = x1 ^ y1 ) ) & ( for v, w being Point of [:(product X),Y:] holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Point of [:(product X),Y:]
for r being Element of REAL holds I . (r * v) = r * (I . v) ) & I . (0. [:(product X),Y:]) = 0. (product (X ^ <*Y*>)) )
let Y be RealLinearSpace; ex I being Function of [:(product X),Y:],(product (X ^ <*Y*>)) st
( I is one-to-one & I is onto & ( for x being Point of (product X)
for y being Point of Y ex x1, y1 being FinSequence st
( x = x1 & <*y*> = y1 & I . (x,y) = x1 ^ y1 ) ) & ( for v, w being Point of [:(product X),Y:] holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Point of [:(product X),Y:]
for r being Element of REAL holds I . (r * v) = r * (I . v) ) & I . (0. [:(product X),Y:]) = 0. (product (X ^ <*Y*>)) )
consider I being Function of [:(product X),Y:],[:(product X),(product <*Y*>):] such that
A1:
( I is one-to-one & I is onto & ( for x being Point of (product X)
for y being Point of Y holds I . (x,y) = [x,<*y*>] ) & ( for v, w being Point of [:(product X),Y:] holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Point of [:(product X),Y:]
for r being Element of REAL holds I . (r * v) = r * (I . v) ) & I . (0. [:(product X),Y:]) = 0. [:(product X),(product <*Y*>):] )
by Th21;
consider J being Function of [:(product X),(product <*Y*>):],(product (X ^ <*Y*>)) such that
A2:
( J is one-to-one & J is onto & ( for x being Point of (product X)
for y being Point of (product <*Y*>) ex x1, y1 being FinSequence st
( x = x1 & y = y1 & J . (x,y) = x1 ^ y1 ) ) & ( for v, w being Point of [:(product X),(product <*Y*>):] holds J . (v + w) = (J . v) + (J . w) ) & ( for v being Point of [:(product X),(product <*Y*>):]
for r being Element of REAL holds J . (r * v) = r * (J . v) ) & J . (0. [:(product X),(product <*Y*>):]) = 0. (product (X ^ <*Y*>)) )
by Th13;
set K = J * I;
reconsider K = J * I as Function of [:(product X),Y:],(product (X ^ <*Y*>)) ;
take
K
; ( K is one-to-one & K is onto & ( for x being Point of (product X)
for y being Point of Y ex x1, y1 being FinSequence st
( x = x1 & <*y*> = y1 & K . (x,y) = x1 ^ y1 ) ) & ( for v, w being Point of [:(product X),Y:] holds K . (v + w) = (K . v) + (K . w) ) & ( for v being Point of [:(product X),Y:]
for r being Element of REAL holds K . (r * v) = r * (K . v) ) & K . (0. [:(product X),Y:]) = 0. (product (X ^ <*Y*>)) )
thus
K is one-to-one
by A1, A2; ( K is onto & ( for x being Point of (product X)
for y being Point of Y ex x1, y1 being FinSequence st
( x = x1 & <*y*> = y1 & K . (x,y) = x1 ^ y1 ) ) & ( for v, w being Point of [:(product X),Y:] holds K . (v + w) = (K . v) + (K . w) ) & ( for v being Point of [:(product X),Y:]
for r being Element of REAL holds K . (r * v) = r * (K . v) ) & K . (0. [:(product X),Y:]) = 0. (product (X ^ <*Y*>)) )
A3:
rng J = the carrier of (product (X ^ <*Y*>))
by A2, FUNCT_2:def 3;
rng I = the carrier of [:(product X),(product <*Y*>):]
by A1, FUNCT_2:def 3;
then rng (J * I) =
J .: the carrier of [:(product X),(product <*Y*>):]
by RELAT_1:127
.=
the carrier of (product (X ^ <*Y*>))
by A3, RELSET_1:22
;
hence
K is onto
by FUNCT_2:def 3; ( ( for x being Point of (product X)
for y being Point of Y ex x1, y1 being FinSequence st
( x = x1 & <*y*> = y1 & K . (x,y) = x1 ^ y1 ) ) & ( for v, w being Point of [:(product X),Y:] holds K . (v + w) = (K . v) + (K . w) ) & ( for v being Point of [:(product X),Y:]
for r being Element of REAL holds K . (r * v) = r * (K . v) ) & K . (0. [:(product X),Y:]) = 0. (product (X ^ <*Y*>)) )
thus
for x being Point of (product X)
for y being Point of Y ex x1, y1 being FinSequence st
( x = x1 & <*y*> = y1 & K . (x,y) = x1 ^ y1 )
( ( for v, w being Point of [:(product X),Y:] holds K . (v + w) = (K . v) + (K . w) ) & ( for v being Point of [:(product X),Y:]
for r being Element of REAL holds K . (r * v) = r * (K . v) ) & K . (0. [:(product X),Y:]) = 0. (product (X ^ <*Y*>)) )proof
let x be
Point of
(product X);
for y being Point of Y ex x1, y1 being FinSequence st
( x = x1 & <*y*> = y1 & K . (x,y) = x1 ^ y1 )let y be
Point of
Y;
ex x1, y1 being FinSequence st
( x = x1 & <*y*> = y1 & K . (x,y) = x1 ^ y1 )
A4:
I . (
x,
y)
= [x,<*y*>]
by A1;
[x,y] in the
carrier of
[:(product X),Y:]
;
then
[x,<*y*>] in the
carrier of
[:(product X),(product <*Y*>):]
by A4, FUNCT_2:5;
then reconsider yy =
<*y*> as
Point of
(product <*Y*>) by ZFMISC_1:87;
consider x1,
y1 being
FinSequence such that A5:
(
x = x1 &
yy = y1 &
J . (
x,
yy)
= x1 ^ y1 )
by A2;
J . (
x,
yy) =
J . (I . [x,y])
by A4
.=
K . (
x,
y)
by FUNCT_2:15
;
hence
ex
x1,
y1 being
FinSequence st
(
x = x1 &
<*y*> = y1 &
K . (
x,
y)
= x1 ^ y1 )
by A5;
verum
end;
thus
for v, w being Point of [:(product X),Y:] holds K . (v + w) = (K . v) + (K . w)
( ( for v being Point of [:(product X),Y:]
for r being Element of REAL holds K . (r * v) = r * (K . v) ) & K . (0. [:(product X),Y:]) = 0. (product (X ^ <*Y*>)) )
thus
for v being Point of [:(product X),Y:]
for r being Element of REAL holds K . (r * v) = r * (K . v)
K . (0. [:(product X),Y:]) = 0. (product (X ^ <*Y*>))
thus
K . (0. [:(product X),Y:]) = 0. (product (X ^ <*Y*>))
by A1, A2, FUNCT_2:15; verum