let X be set ; 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; ( 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
; 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 ;
TARSKI:def 3 ( not x in Y /\ (dom f2) or x in g2 " X )
assume A7:
x in Y /\ (dom f2)
;
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;
verum
end;
A13:
dom f1 = dom g1
by A1, FINSEQ_3:29;
A14:
g1 " X c= ((g1 ^ g2) " X) /\ (dom f1)
( 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
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 ;
TARSKI:def 3 ( not x in g2 " X or x in Y /\ (dom f2) )
assume A24:
x in g2 " X
;
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;
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; verum