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 ;
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 ; :: thesis: p2 in product f2
A8: len (f1 ^ f2) = len g by ;
then A9: len f1 = len p1 by ;
len g = (len p1) + (len p2) by ;
then A10: dom f2 = dom p2 by ;
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 ;
then ( g . (i + (len f1)) in (f1 ^ f2) . (i + (len f1)) & (f1 ^ f2) . (i + (len f1)) = f2 . i ) by ;
hence p2 . y in f2 . y by ; :: thesis: verum
end;
hence p2 in product f2 by ; :: 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 ;
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 ;
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) . b1 in (f1 ^ f2) . b1 )
assume A19: y in dom (f1 ^ f2) ; :: thesis: (p1 ^ p2) . b1 in (f1 ^ f2) . b1
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 ;
suppose A20: i in dom f1 ; :: thesis: (p1 ^ p2) . b1 in (f1 ^ f2) . b1
then ( (f1 ^ f2) . y = f1 . i & (p1 ^ p2) . y = p1 . i ) by ;
hence (p1 ^ p2) . y in (f1 ^ f2) . y by ; :: thesis: verum
end;
suppose ex j being Nat st
( j in dom f2 & i = (len f1) + j ) ; :: thesis: (p1 ^ p2) . b1 in (f1 ^ f2) . b1
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 ;
hence (p1 ^ p2) . y in (f1 ^ f2) . y by ; :: thesis: verum
end;
end;
end;
( len (p1 ^ p2) = (len p1) + (len p2) & len p2 = len f2 ) by ;
then dom (p1 ^ p2) = dom (f1 ^ f2) by ;
hence x in product (f1 ^ f2) by ; :: thesis: verum