let X, Y be RealLinearSpace-Sequence; :: thesis: carr (X ^ Y) = (carr X) ^ (carr Y)
reconsider CX = carr X, CY = carr Y as FinSequence ;
A1: ( len CX = len X & len CY = len Y & len (carr (X ^ Y)) = len (X ^ Y) ) by PRVECT_1:def 11;
( len (carr (X ^ Y)) = (len X) + (len Y) & len (CX ^ CY) = (len X) + (len Y) ) by A1, FINSEQ_1:22;
then A2: dom (carr (X ^ Y)) = dom (CX ^ CY) by FINSEQ_3:29;
for i being Nat st i in dom (carr (X ^ Y)) holds
(carr (X ^ Y)) . i = (CX ^ CY) . i

proof

let i be Nat; :: thesis: ( i in dom (carr (X ^ Y)) implies (carr (X ^ Y)) . i = (CX ^ CY) . i )
assume A3: i in dom (carr (X ^ Y)) ; :: thesis: (carr (X ^ Y)) . i = (CX ^ CY) . i
then reconsider i1 = i as Element of dom (X ^ Y) by A1, FINSEQ_3:29;
A4: (carr (X ^ Y)) . i = the carrier of ((X ^ Y) . i1) by PRVECT_1:def 11;
A5: i in dom (X ^ Y) by A1, A3, FINSEQ_3:29;

per cases ( i in dom X or ex n being Nat st
( n in dom Y & i = (len X) + n ) ) by A5, FINSEQ_1:25;

suppose A6: i in dom X ; :: thesis: (carr (X ^ Y)) . i = (CX ^ CY) . i

then A7: i in dom CX by A1, FINSEQ_3:29;
reconsider i2 = i1 as Element of dom X by A6;
thus (carr (X ^ Y)) . i = the carrier of (X . i2) by A4, FINSEQ_1:def 7
.= CX . i by PRVECT_1:def 11
.= (CX ^ CY) . i by A7, FINSEQ_1:def 7 ; :: thesis: verum

end;

suppose ex n being Nat st
( n in dom Y & i = (len X) + n ) ; :: thesis: (carr (X ^ Y)) . i = (CX ^ CY) . i

then consider n being Nat such that
A8: ( n in dom Y & i = (len X) + n ) ;
A9: n in dom CY by A1, A8, FINSEQ_3:29;
reconsider n1 = n as Element of dom Y by A8;
thus (carr (X ^ Y)) . i = the carrier of (Y . n1) by A4, A8, FINSEQ_1:def 7
.= CY . n by PRVECT_1:def 11
.= (CX ^ CY) . i by A1, A8, A9, FINSEQ_1:def 7 ; :: thesis: verum

end;

end;

end;

hence carr (X ^ Y) = (carr X) ^ (carr Y) by A2, FINSEQ_1:13; :: thesis: verum