let X be set ; :: thesis: for f1, f2, g1, g2 being FinSequence st len g1 = len f1 & len g2 <= len f2 holds
Seq ((f1 ^ f2) | ((g1 ^ g2) " X)) = (Seq (f1 | (g1 " X))) ^ (Seq (f2 | (g2 " X)))
let f1, f2, g1, g2 be FinSequence; :: thesis: ( len g1 = len f1 & len g2 <= len f2 implies Seq ((f1 ^ f2) | ((g1 ^ g2) " X)) = (Seq (f1 | (g1 " X))) ^ (Seq (f2 | (g2 " X))) )
assume that
A1: len f1 = len g1 and
A2: len g2 <= len f2 ; :: thesis: Seq ((f1 ^ f2) | ((g1 ^ g2) " X)) = (Seq (f1 | (g1 " X))) ^ (Seq (f2 | (g2 " X)))
set f12 = f1 ^ f2;
set g12 = g1 ^ g2;
A3: ( dom (f1 ^ f2) = Seg (len (f1 ^ f2)) & dom (g1 ^ g2) = Seg (len (g1 ^ g2)) ) by FINSEQ_1:def 3;
set g12X = (g1 ^ g2) " X;
consider Y being Subset of NAT such that
A4: Seq ((f1 ^ f2) | ((g1 ^ g2) " X)) = (Seq (f1 | ((g1 ^ g2) " X))) ^ (Seq (f2 | Y)) and
A5: for n being Nat st n > 0 holds
( n in Y iff n + (len f1) in ((g1 ^ g2) " X) /\ (dom (f1 ^ f2)) ) by Th12;
A6: Y /\ (dom f2) c= g2 " X

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Y /\ (dom f2) or x in g2 " X )
assume A7: x in Y /\ (dom f2) ; :: thesis: x in g2 " X
then reconsider i = x as Nat ;
x in dom f2 by A7, XBOOLE_0:def 4;
then A8: i > 0 by FINSEQ_3:25;
then i + (len f1) > (len f1) + 0 by XREAL_1:6;
then A9: not i + (len f1) in dom g1 by A1, FINSEQ_3:25;
x in Y by A7, XBOOLE_0:def 4;
then i + (len f1) in ((g1 ^ g2) " X) /\ (dom (f1 ^ f2)) by A5, A8;
then A10: i + (len f1) in (g1 ^ g2) " X by XBOOLE_0:def 4;
then A11: (g1 ^ g2) . (i + (len f1)) in X by FUNCT_1:def 7;
i + (len f1) in dom (g1 ^ g2) by A10, FUNCT_1:def 7;
then A12: ex j being Nat st
( j in dom g2 & i + (len f1) = (len g1) + j ) by A9, FINSEQ_1:25;
then (g1 ^ g2) . (i + (len f1)) = g2 . i by A1, FINSEQ_1:def 7;
hence x in g2 " X by A1, A11, A12, FUNCT_1:def 7; :: thesis: verum

end;

A13: dom f1 = dom g1 by A1, FINSEQ_3:29;
A14: g1 " X c= ((g1 ^ g2) " X) /\ (dom f1)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in g1 " X or x in ((g1 ^ g2) " X) /\ (dom f1) )
assume A15: x in g1 " X ; :: thesis: x in ((g1 ^ g2) " X) /\ (dom f1)
then A16: x in dom g1 by FUNCT_1:def 7;
A17: g1 . x in X by A15, FUNCT_1:def 7;
( dom g1 c= dom (g1 ^ g2) & (g1 ^ g2) . x = g1 . x ) by A16, FINSEQ_1:26, FINSEQ_1:def 7;
then x in (g1 ^ g2) " X by A16, A17, FUNCT_1:def 7;
hence x in ((g1 ^ g2) " X) /\ (dom f1) by A13, A16, XBOOLE_0:def 4; :: thesis: verum

end;

( len (f1 ^ f2) = (len f1) + (len f2) & len (g1 ^ g2) = (len g1) + (len g2) ) by FINSEQ_1:22;
then len (g1 ^ g2) <= len (f1 ^ f2) by A1, A2, XREAL_1:6;
then A18: dom (g1 ^ g2) c= dom (f1 ^ f2) by A3, FINSEQ_1:5;
((g1 ^ g2) " X) /\ (dom f1) c= g1 " X

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ((g1 ^ g2) " X) /\ (dom f1) or x in g1 " X )
assume A19: x in ((g1 ^ g2) " X) /\ (dom f1) ; :: thesis: x in g1 " X
then x in (g1 ^ g2) " X by XBOOLE_0:def 4;
then A20: (g1 ^ g2) . x in X by FUNCT_1:def 7;
A21: x in dom f1 by A19, XBOOLE_0:def 4;
then (g1 ^ g2) . x = g1 . x by A13, FINSEQ_1:def 7;
hence x in g1 " X by A13, A21, A20, FUNCT_1:def 7; :: thesis: verum

end;

then ((g1 ^ g2) " X) /\ (dom f1) = g1 " X by A14;
then A22: f1 | (g1 " X) = f1 | ((g1 ^ g2) " X) by RELAT_1:157;
( dom f2 = Seg (len f2) & dom g2 = Seg (len g2) ) by FINSEQ_1:def 3;
then A23: dom g2 c= dom f2 by A2, FINSEQ_1:5;
g2 " X c= Y /\ (dom f2)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in g2 " X or x in Y /\ (dom f2) )
assume A24: x in g2 " X ; :: thesis: x in Y /\ (dom f2)
then A25: x in dom g2 by FUNCT_1:def 7;
then reconsider i = x as Nat ;
A26: g2 . x in X by A24, FUNCT_1:def 7;
A27: i + (len g1) in dom (g1 ^ g2) by A25, FINSEQ_1:28;
(g1 ^ g2) . (i + (len g1)) = g2 . i by A25, FINSEQ_1:def 7;
then i + (len g1) in (g1 ^ g2) " X by A26, A27, FUNCT_1:def 7;
then A28: i + (len g1) in ((g1 ^ g2) " X) /\ (dom (f1 ^ f2)) by A18, A27, XBOOLE_0:def 4;
i > 0 by A25, FINSEQ_3:25;
then i in Y by A1, A5, A28;
hence x in Y /\ (dom f2) by A23, A25, XBOOLE_0:def 4; :: thesis: verum

end;

then Y /\ (dom f2) = g2 " X by A6;
hence Seq ((f1 ^ f2) | ((g1 ^ g2) " X)) = (Seq (f1 | (g1 " X))) ^ (Seq (f2 | (g2 " X))) by A4, A22, RELAT_1:157; :: thesis: verum