let x be set ; :: thesis: for f1, f2 being FinSequence holds
( x in product (f1 ^ f2) iff ex p1, p2 being FinSequence st
( x = p1 ^ p2 & p1 in product f1 & p2 in product f2 ) )
let f1, f2 be FinSequence; :: thesis: ( x in product (f1 ^ f2) iff ex p1, p2 being FinSequence st
( x = p1 ^ p2 & p1 in product f1 & p2 in product f2 ) )
set f12 = f1 ^ f2;
A1: len (f1 ^ f2) = (len f1) + (len f2) by FINSEQ_1:22;
dom f1 = Seg (len f1) by FINSEQ_1:def 3;
then A2: (f1 ^ f2) | (Seg (len f1)) = f1 by FINSEQ_1:21;

hereby :: thesis: ( ex p1, p2 being FinSequence st
( x = p1 ^ p2 & p1 in product f1 & p2 in product f2 ) implies x in product (f1 ^ f2) )

assume A3: x in product (f1 ^ f2) ; :: thesis: ex p1 being set ex p2 being FinSequence st
( x = p1 ^ p2 & p1 in product f1 & p2 in product f2 )
then consider g being Function such that
A4: x = g and
A5: dom g = dom (f1 ^ f2) and
A6: for y being object st y in dom (f1 ^ f2) holds
g . y in (f1 ^ f2) . y by CARD_3:def 5;
dom (f1 ^ f2) = Seg (len (f1 ^ f2)) by FINSEQ_1:def 3;
then reconsider g = g as FinSequence by A5, FINSEQ_1:def 2;
set p1 = g | (len f1);
consider p2 being FinSequence such that
A7: g = (g | (len f1)) ^ p2 by FINSEQ_1:80;
take p1 = g | (len f1); :: thesis: ex p2 being FinSequence st
( x = p1 ^ p2 & p1 in product f1 & p2 in product f2 )
take p2 = p2; :: thesis: ( x = p1 ^ p2 & p1 in product f1 & p2 in product f2 )
thus ( x = p1 ^ p2 & p1 in product f1 ) by A2, A3, A4, A7, PRALG_3:1; :: thesis: p2 in product f2
A8: len (f1 ^ f2) = len g by A5, FINSEQ_3:29;
then A9: len f1 = len p1 by A1, FINSEQ_1:59, NAT_1:11;
len g = (len p1) + (len p2) by A7, FINSEQ_1:22;
then A10: dom f2 = dom p2 by A1, A8, A9, FINSEQ_3:29;

now :: thesis: for y being object st y in dom f2 holds
p2 . y in f2 . y

let y be object ; :: thesis: ( y in dom f2 implies p2 . y in f2 . y )
assume A11: y in dom f2 ; :: thesis: p2 . y in f2 . y
then reconsider i = y as Nat ;
i + (len f1) in dom (f1 ^ f2) by A11, FINSEQ_1:28;
then ( g . (i + (len f1)) in (f1 ^ f2) . (i + (len f1)) & (f1 ^ f2) . (i + (len f1)) = f2 . i ) by A6, A11, FINSEQ_1:def 7;
hence p2 . y in f2 . y by A7, A9, A10, A11, FINSEQ_1:def 7; :: thesis: verum

end;

hence p2 in product f2 by A10, CARD_3:def 5; :: thesis: verum

end;

given p1, p2 being FinSequence such that A12: x = p1 ^ p2 and
A13: p1 in product f1 and
A14: p2 in product f2 ; :: thesis: x in product (f1 ^ f2)
A15: ex g being Function st
( p2 = g & dom g = dom f2 & ( for y being object st y in dom f2 holds
g . y in f2 . y ) ) by A14, CARD_3:def 5;
A16: ex g being Function st
( p1 = g & dom g = dom f1 & ( for y being object st y in dom f1 holds
g . y in f1 . y ) ) by A13, CARD_3:def 5;
then A17: len p1 = len f1 by FINSEQ_3:29;

A18: now :: thesis: for y being object st y in dom (f1 ^ f2) holds
(p1 ^ p2) . y in (f1 ^ f2) . y

let y be object ; :: thesis: ( y in dom (f1 ^ f2) implies (p1 ^ p2) . b₁ in (f1 ^ f2) . b₁ )
assume A19: y in dom (f1 ^ f2) ; :: thesis: (p1 ^ p2) . b₁ in (f1 ^ f2) . b₁
then reconsider i = y as Nat ;

per cases ( i in dom f1 or ex j being Nat st
( j in dom f2 & i = (len f1) + j ) ) by A19, FINSEQ_1:25;

suppose A20: i in dom f1 ; :: thesis: (p1 ^ p2) . b₁ in (f1 ^ f2) . b₁

then ( (f1 ^ f2) . y = f1 . i & (p1 ^ p2) . y = p1 . i ) by A16, FINSEQ_1:def 7;
hence (p1 ^ p2) . y in (f1 ^ f2) . y by A16, A20; :: thesis: verum

end;

suppose ex j being Nat st
( j in dom f2 & i = (len f1) + j ) ; :: thesis: (p1 ^ p2) . b₁ in (f1 ^ f2) . b₁

then consider j being Nat such that
A21: j in dom f2 and
A22: i = (len f1) + j ;
( (f1 ^ f2) . y = f2 . j & (p1 ^ p2) . y = p2 . j ) by A15, A17, A21, A22, FINSEQ_1:def 7;
hence (p1 ^ p2) . y in (f1 ^ f2) . y by A15, A21; :: thesis: verum

end;

end;

end;

( len (p1 ^ p2) = (len p1) + (len p2) & len p2 = len f2 ) by A15, FINSEQ_1:22, FINSEQ_3:29;
then dom (p1 ^ p2) = dom (f1 ^ f2) by A1, A17, FINSEQ_3:29;
hence x in product (f1 ^ f2) by A12, A18, CARD_3:def 5; :: thesis: verum