let X be RealNormSpace-Sequence; :: thesis: for x being Element of (product X)
for Y being RealNormSpace
for y being Point of Y holds x ^ <*y*> is Point of (product (X ^ <*Y*>))
let x be Element of (product X); :: thesis: for Y being RealNormSpace
for y being Point of Y holds x ^ <*y*> is Point of (product (X ^ <*Y*>))
let Y be RealNormSpace; :: thesis: for y being Point of Y holds x ^ <*y*> is Point of (product (X ^ <*Y*>))
let y be Point of Y; :: thesis: x ^ <*y*> is Point of (product (X ^ <*Y*>))
set CX = carr X;
set CY = the carrier of Y;
A1: product X = NORMSTR(# (product (carr X)),(zeros X),[:(addop X):],[:(multop X):],(productnorm X) #) by PRVECT_2:6;
product (X ^ <*Y*>) = NORMSTR(# (product (carr (X ^ <*Y*>))),(zeros (X ^ <*Y*>)),[:(addop (X ^ <*Y*>)):],[:(multop (X ^ <*Y*>)):],(productnorm (X ^ <*Y*>)) #) by PRVECT_2:6;
then A2: the carrier of (product (X ^ <*Y*>)) = product ((carr X) ^ (carr <*Y*>)) by Th30
.= product ((carr X) ^ <* the carrier of Y*>) by Th31 ;
A3: ex x1 being Function st
( x = x1 & dom x1 = dom (carr X) & ( for i being object st i in dom (carr X) holds
x1 . i in (carr X) . i ) ) by A1, CARD_3:def 5;
A4: len (x ^ <*y*>) = (len x) + (len <*y*>) by FINSEQ_1:22
.= (len x) + 1 by FINSEQ_1:40 ;
A5: dom x = Seg (len (carr X)) by A3, FINSEQ_1:def 3;
then A6: len x = len (carr X) by FINSEQ_1:def 3;
A7: len ((carr X) ^ <* the carrier of Y*>) = (len (carr X)) + (len <* the carrier of Y*>) by FINSEQ_1:22
.= (len (carr X)) + 1 by FINSEQ_1:40 ;
A8: dom (x ^ <*y*>) = Seg (len (x ^ <*y*>)) by FINSEQ_1:def 3
.= Seg (len ((carr X) ^ <* the carrier of Y*>)) by A4, A5, A7, FINSEQ_1:def 3
.= dom ((carr X) ^ <* the carrier of Y*>) by FINSEQ_1:def 3 ;
for i being object st i in dom ((carr X) ^ <* the carrier of Y*>) holds
(x ^ <*y*>) . i in ((carr X) ^ <* the carrier of Y*>) . i

proof

let i be object ; :: thesis: ( i in dom ((carr X) ^ <* the carrier of Y*>) implies (x ^ <*y*>) . i in ((carr X) ^ <* the carrier of Y*>) . i )
assume A9: i in dom ((carr X) ^ <* the carrier of Y*>) ; :: thesis: (x ^ <*y*>) . i in ((carr X) ^ <* the carrier of Y*>) . i
then A10: i in Seg (len ((carr X) ^ <* the carrier of Y*>)) by FINSEQ_1:def 3;
reconsider i1 = i as Nat by A9;

per cases ( i1 <= len x or len x < i1 ) ;

suppose A11: i1 <= len x ; :: thesis: (x ^ <*y*>) . i in ((carr X) ^ <* the carrier of Y*>) . i

( 1 <= i1 & i1 <= len ((carr X) ^ <* the carrier of Y*>) ) by A10, FINSEQ_1:1;
then A12: i1 in Seg (len x) by A11;
then i1 in dom x by FINSEQ_1:def 3;
then A13: (x ^ <*y*>) . i1 = x . i1 by FINSEQ_1:def 7;
A15: i1 in dom (carr X) by A3, FINSEQ_1:def 3, A12;
i1 in dom x by A12, FINSEQ_1:def 3;
then x . i1 in (carr X) . i1 by A3;
hence (x ^ <*y*>) . i in ((carr X) ^ <* the carrier of Y*>) . i by A13, A15, FINSEQ_1:def 7; :: thesis: verum

end;

suppose len x < i1 ; :: thesis: (x ^ <*y*>) . i in ((carr X) ^ <* the carrier of Y*>) . i

then A17: (len x) + 1 <= i1 by NAT_1:13;
( 1 <= i1 & i1 <= len ((carr X) ^ <* the carrier of Y*>) ) by A10, FINSEQ_1:1;
then A19: i1 = (len x) + 1 by A6, A7, A17, XXREAL_0:1;
then A20: (x ^ <*y*>) . i1 = y by FINSEQ_1:42;
((carr X) ^ <* the carrier of Y*>) . i1 = the carrier of Y by A6, A19, FINSEQ_1:42;
hence (x ^ <*y*>) . i in ((carr X) ^ <* the carrier of Y*>) . i by A20; :: thesis: verum

end;

end;

end;

hence x ^ <*y*> is Point of (product (X ^ <*Y*>)) by A2, A8, CARD_3:def 5; :: thesis: verum