let X be set ; :: thesis: for f1, f2 being FinSequence ex Y being Subset of NAT st
( Seq ((f1 ^ f2) | X) = (Seq (f1 | X)) ^ (Seq (f2 | Y)) & ( for n being Nat st n > 0 holds
( n in Y iff n + (len f1) in X /\ (dom (f1 ^ f2)) ) ) )
let f1, f2 be FinSequence; :: thesis: ex Y being Subset of NAT st
( Seq ((f1 ^ f2) | X) = (Seq (f1 | X)) ^ (Seq (f2 | Y)) & ( for n being Nat st n > 0 holds
( n in Y iff n + (len f1) in X /\ (dom (f1 ^ f2)) ) ) )
set f12 = f1 ^ f2;
set n1 = len f1;
set n2 = len f2;
set X12 = X /\ (dom (f1 ^ f2));
set X1 = (X /\ (dom (f1 ^ f2))) /\ (Seg (len f1));
set X2 = (X /\ (dom (f1 ^ f2))) \ (Seg (len f1));
set Y2 = { i where i is Element of NAT : i + (len f1) in (X /\ (dom (f1 ^ f2))) \ (Seg (len f1)) } ;
{ i where i is Element of NAT : i + (len f1) in (X /\ (dom (f1 ^ f2))) \ (Seg (len f1)) } c= NAT
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { i where i is Element of NAT : i + (len f1) in (X /\ (dom (f1 ^ f2))) \ (Seg (len f1)) } or x in NAT )
assume x in { i where i is Element of NAT : i + (len f1) in (X /\ (dom (f1 ^ f2))) \ (Seg (len f1)) } ; :: thesis: x in NAT
then ex i being Element of NAT st
( i = x & i + (len f1) in (X /\ (dom (f1 ^ f2))) \ (Seg (len f1)) ) ;
hence x in NAT ; :: thesis: verum
end;
then reconsider Y2 = { i where i is Element of NAT : i + (len f1) in (X /\ (dom (f1 ^ f2))) \ (Seg (len f1)) } as Subset of NAT ;
set Sf2 = (len f1) Shift f2;
A1: f1 ^ f2 = f1 \/ ((len f1) Shift f2) by VALUED_1:49;
take Y2 ; :: thesis: ( Seq ((f1 ^ f2) | X) = (Seq (f1 | X)) ^ (Seq (f2 | Y2)) & ( for n being Nat st n > 0 holds
( n in Y2 iff n + (len f1) in X /\ (dom (f1 ^ f2)) ) ) )
A2: (X /\ (dom (f1 ^ f2))) /\ (dom ((len f1) Shift f2)) c= (X /\ (dom (f1 ^ f2))) \ (Seg (len f1))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (X /\ (dom (f1 ^ f2))) /\ (dom ((len f1) Shift f2)) or x in (X /\ (dom (f1 ^ f2))) \ (Seg (len f1)) )
assume A3: x in (X /\ (dom (f1 ^ f2))) /\ (dom ((len f1) Shift f2)) ; :: thesis: x in (X /\ (dom (f1 ^ f2))) \ (Seg (len f1))
then x in dom ((len f1) Shift f2) by XBOOLE_0:def 4;
then x in { (k + (len f1)) where k is Nat : k in dom f2 } by VALUED_1:def 12;
then consider k being Nat such that
A4: x = k + (len f1) and
A5: k in dom f2 ;
1 <= k by A5, FINSEQ_3:25;
then 1 + (len f1) <= k + (len f1) by XREAL_1:6;
then len f1 < k + (len f1) by NAT_1:13;
then A6: not x in Seg (len f1) by A4, FINSEQ_1:1;
x in X /\ (dom (f1 ^ f2)) by A3, XBOOLE_0:def 4;
hence x in (X /\ (dom (f1 ^ f2))) \ (Seg (len f1)) by A6, XBOOLE_0:def 5; :: thesis: verum
end;
A7: now :: thesis: for i being Nat holds
( ( i + (len f1) in (X /\ (dom (f1 ^ f2))) \ (Seg (len f1)) implies i in Y2 ) & ( i in Y2 implies i + (len f1) in (X /\ (dom (f1 ^ f2))) \ (Seg (len f1)) ) )
let i be Nat; :: thesis: ( ( i + (len f1) in (X /\ (dom (f1 ^ f2))) \ (Seg (len f1)) implies i in Y2 ) & ( i in Y2 implies i + (len f1) in (X /\ (dom (f1 ^ f2))) \ (Seg (len f1)) ) )
thus ( i + (len f1) in (X /\ (dom (f1 ^ f2))) \ (Seg (len f1)) implies i in Y2 ) :: thesis: ( i in Y2 implies i + (len f1) in (X /\ (dom (f1 ^ f2))) \ (Seg (len f1)) )
proof
assume A8: i + (len f1) in (X /\ (dom (f1 ^ f2))) \ (Seg (len f1)) ; :: thesis: i in Y2
i in NAT by ORDINAL1:def 12;
hence i in Y2 by A8; :: thesis: verum
end;
assume i in Y2 ; :: thesis: i + (len f1) in (X /\ (dom (f1 ^ f2))) \ (Seg (len f1))
then ex j being Element of NAT st
( i = j & j + (len f1) in (X /\ (dom (f1 ^ f2))) \ (Seg (len f1)) ) ;
hence i + (len f1) in (X /\ (dom (f1 ^ f2))) \ (Seg (len f1)) ; :: thesis: verum
end;
( f1 | ((X /\ (dom (f1 ^ f2))) /\ (Seg (len f1))) c= f1 & f2 | Y2 c= f2 ) by RELAT_1:59;
then consider ss being FinSubsequence such that
A9: ( ss = (f1 | ((X /\ (dom (f1 ^ f2))) /\ (Seg (len f1)))) \/ ((len f1) Shift (f2 | Y2)) & (Seq (f1 | ((X /\ (dom (f1 ^ f2))) /\ (Seg (len f1))))) ^ (Seq (f2 | Y2)) = Seq ss ) by VALUED_1:64;
A10: dom f1 = Seg (len f1) by FINSEQ_1:def 3;
then (dom (f1 ^ f2)) /\ (Seg (len f1)) = Seg (len f1) by FINSEQ_1:26, XBOOLE_1:28;
then A11: f1 | X = f1 | (X /\ ((dom (f1 ^ f2)) /\ (Seg (len f1)))) by A10, RELAT_1:157
.= f1 | ((X /\ (dom (f1 ^ f2))) /\ (Seg (len f1))) by XBOOLE_1:16 ;
(X /\ (dom (f1 ^ f2))) \ (Seg (len f1)) c= (X /\ (dom (f1 ^ f2))) /\ (dom ((len f1) Shift f2))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (X /\ (dom (f1 ^ f2))) \ (Seg (len f1)) or x in (X /\ (dom (f1 ^ f2))) /\ (dom ((len f1) Shift f2)) )
assume A12: x in (X /\ (dom (f1 ^ f2))) \ (Seg (len f1)) ; :: thesis: x in (X /\ (dom (f1 ^ f2))) /\ (dom ((len f1) Shift f2))
then A13: not x in Seg (len f1) by XBOOLE_0:def 5;
A14: x in X /\ (dom (f1 ^ f2)) by A12, XBOOLE_0:def 5;
then x in dom (f1 ^ f2) by XBOOLE_0:def 4;
then consider k being Nat such that
A15: ( k in dom f2 & x = (len f1) + k ) by A10, A13, FINSEQ_1:25;
x in { (i + (len f1)) where i is Nat : i in dom f2 } by A15;
then x in dom ((len f1) Shift f2) by VALUED_1:def 12;
hence x in (X /\ (dom (f1 ^ f2))) /\ (dom ((len f1) Shift f2)) by A14, XBOOLE_0:def 4; :: thesis: verum
end;
then A16: (X /\ (dom (f1 ^ f2))) \ (Seg (len f1)) = (X /\ (dom (f1 ^ f2))) /\ (dom ((len f1) Shift f2)) by A2;
(f1 ^ f2) | X = (f1 ^ f2) | (X /\ (dom (f1 ^ f2))) by RELAT_1:157;
then (f1 ^ f2) | X = (f1 ^ f2) * (id (X /\ (dom (f1 ^ f2)))) by RELAT_1:65
.= (f1 * (id (X /\ (dom (f1 ^ f2))))) \/ (((len f1) Shift f2) * (id (X /\ (dom (f1 ^ f2))))) by A1, RELAT_1:32
.= (f1 | (X /\ (dom (f1 ^ f2)))) \/ (((len f1) Shift f2) * (id (X /\ (dom (f1 ^ f2))))) by RELAT_1:65
.= (f1 | (X /\ (dom (f1 ^ f2)))) \/ (((len f1) Shift f2) | (X /\ (dom (f1 ^ f2)))) by RELAT_1:65
.= (f1 | (X /\ (dom (f1 ^ f2)))) \/ (((len f1) Shift f2) | ((X /\ (dom (f1 ^ f2))) \ (Seg (len f1)))) by A16, RELAT_1:157
.= (f1 | ((X /\ (dom (f1 ^ f2))) /\ (Seg (len f1)))) \/ (((len f1) Shift f2) | ((X /\ (dom (f1 ^ f2))) \ (Seg (len f1)))) by A10, RELAT_1:157 ;
hence Seq ((f1 ^ f2) | X) = (Seq (f1 | X)) ^ (Seq (f2 | Y2)) by A7, A11, A9, Th11; :: thesis: for n being Nat st n > 0 holds
( n in Y2 iff n + (len f1) in X /\ (dom (f1 ^ f2)) )
let n be Nat; :: thesis: ( n > 0 implies ( n in Y2 iff n + (len f1) in X /\ (dom (f1 ^ f2)) ) )
assume n > 0 ; :: thesis: ( n in Y2 iff n + (len f1) in X /\ (dom (f1 ^ f2)) )
then n + (len f1) > 0 + (len f1) by XREAL_1:6;
then A17: not n + (len f1) in Seg (len f1) by FINSEQ_1:1;
hereby :: thesis: ( n + (len f1) in X /\ (dom (f1 ^ f2)) implies n in Y2 )
assume n in Y2 ; :: thesis: n + (len f1) in X /\ (dom (f1 ^ f2))
then n + (len f1) in (X /\ (dom (f1 ^ f2))) \ (Seg (len f1)) by A7;
hence n + (len f1) in X /\ (dom (f1 ^ f2)) by XBOOLE_0:def 5; :: thesis: verum
end;
assume n + (len f1) in X /\ (dom (f1 ^ f2)) ; :: thesis: n in Y2
then n + (len f1) in (X /\ (dom (f1 ^ f2))) \ (Seg (len f1)) by A17, XBOOLE_0:def 5;
hence n in Y2 by A7; :: thesis: verum