let f1, f2 be FinSequence; :: thesis: for i being Nat holds (f1 ^ f2) | (Seg ((len f1) + i)) = f1 ^ (f2 | (Seg i))
let i be Nat; :: thesis: (f1 ^ f2) | (Seg ((len f1) + i)) = f1 ^ (f2 | (Seg i))
A1: dom (f1 ^ (f2 | (Seg i))) c= Seg ((len f1) + i)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom (f1 ^ (f2 | (Seg i))) or x in Seg ((len f1) + i) )
assume A2: x in dom (f1 ^ (f2 | (Seg i))) ; :: thesis: x in Seg ((len f1) + i)
then reconsider j = x as Nat ;

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

suppose A3: j in dom f1 ; :: thesis: x in Seg ((len f1) + i)

len f1 <= (len f1) + i by NAT_1:11;
then A4: Seg (len f1) c= Seg ((len f1) + i) by FINSEQ_1:5;
j in Seg (len f1) by A3, FINSEQ_1:def 3;
hence x in Seg ((len f1) + i) by A4; :: thesis: verum

end;

suppose ex n being Nat st
( n in dom (f2 | (Seg i)) & j = (len f1) + n ) ; :: thesis: x in Seg ((len f1) + i)

then consider k being Nat such that
A5: k in dom (f2 | (Seg i)) and
A6: j = (len f1) + k ;
A7: k <= j by A6, NAT_1:11;
dom (f2 | (Seg i)) = (dom f2) /\ (Seg i) by RELAT_1:61;
then k in Seg i by A5, XBOOLE_0:def 4;
then k <= i by FINSEQ_1:1;
then A8: j <= (len f1) + i by A6, XREAL_1:6;
1 <= k by A5, FINSEQ_3:25;
then 1 <= j by A7, XXREAL_0:2;
hence x in Seg ((len f1) + i) by A8; :: thesis: verum

end;

end;

end;

A9: (dom (f1 ^ f2)) /\ (Seg ((len f1) + i)) c= dom (f1 ^ (f2 | (Seg i)))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (dom (f1 ^ f2)) /\ (Seg ((len f1) + i)) or x in dom (f1 ^ (f2 | (Seg i))) )
assume A10: x in (dom (f1 ^ f2)) /\ (Seg ((len f1) + i)) ; :: thesis: x in dom (f1 ^ (f2 | (Seg i)))
then A11: x in dom (f1 ^ f2) by XBOOLE_0:def 4;
reconsider j = x as Nat by A10;

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

suppose A12: j in dom f1 ; :: thesis: x in dom (f1 ^ (f2 | (Seg i)))

dom f1 c= dom (f1 ^ (f2 | (Seg i))) by FINSEQ_1:26;
hence x in dom (f1 ^ (f2 | (Seg i))) by A12; :: thesis: verum

end;

suppose ex n being Nat st
( n in dom f2 & j = (len f1) + n ) ; :: thesis: x in dom (f1 ^ (f2 | (Seg i)))

then consider k being Nat such that
A13: k in dom f2 and
A14: j = (len f1) + k ;
A15: 1 <= k by A13, FINSEQ_3:25;
A16: dom (f2 | (Seg i)) = (dom f2) /\ (Seg i) by RELAT_1:61;
j in Seg ((len f1) + i) by A10, XBOOLE_0:def 4;
then j <= (len f1) + i by FINSEQ_1:1;
then k <= i by A14, XREAL_1:6;
then k in Seg i by A15;
then k in dom (f2 | (Seg i)) by A13, A16, XBOOLE_0:def 4;
hence x in dom (f1 ^ (f2 | (Seg i))) by A14, FINSEQ_1:28; :: thesis: verum

end;

end;

end;

A17: dom ((f1 ^ f2) | (Seg ((len f1) + i))) = (dom (f1 ^ f2)) /\ (Seg ((len f1) + i)) by RELAT_1:61;

A18: now :: thesis: for k being Nat st k in dom ((f1 ^ f2) | (Seg ((len f1) + i))) holds
((f1 ^ f2) | (Seg ((len f1) + i))) . k = (f1 ^ (f2 | (Seg i))) . k

let k be Nat; :: thesis: ( k in dom ((f1 ^ f2) | (Seg ((len f1) + i))) implies ((f1 ^ f2) | (Seg ((len f1) + i))) . b₁ = (f1 ^ (f2 | (Seg i))) . b₁ )
assume A19: k in dom ((f1 ^ f2) | (Seg ((len f1) + i))) ; :: thesis: ((f1 ^ f2) | (Seg ((len f1) + i))) . b₁ = (f1 ^ (f2 | (Seg i))) . b₁
then A20: 1 <= k by FINSEQ_3:25;

per cases ( k <= len f1 or k > len f1 ) ;

suppose k <= len f1 ; :: thesis: ((f1 ^ f2) | (Seg ((len f1) + i))) . b₁ = (f1 ^ (f2 | (Seg i))) . b₁

then A21: k in dom f1 by A20, FINSEQ_3:25;
thus ((f1 ^ f2) | (Seg ((len f1) + i))) . k = (f1 ^ f2) . k by A19, FUNCT_1:47
.= f1 . k by A21, FINSEQ_1:def 7
.= (f1 ^ (f2 | (Seg i))) . k by A21, FINSEQ_1:def 7 ; :: thesis: verum

end;

suppose A22: k > len f1 ; :: thesis: ((f1 ^ f2) | (Seg ((len f1) + i))) . b₁ = (f1 ^ (f2 | (Seg i))) . b₁

then reconsider j = k - (len f1) as Element of NAT by INT_1:5;
j > 0 by A22, XREAL_1:50;
then A23: 1 <= j by NAT_1:14;
A24: k = (len f1) + j ;
A25: not k in dom f1 by A22, FINSEQ_3:25;
k in dom (f1 ^ f2) by A17, A19, XBOOLE_0:def 4;
then A26: ex n being Nat st
( n in dom f2 & k = (len f1) + n ) by A25, FINSEQ_1:25;
k in Seg ((len f1) + i) by A17, A19, XBOOLE_0:def 4;
then k <= (len f1) + i by FINSEQ_1:1;
then j <= i by A24, XREAL_1:6;
then A27: j in Seg i by A23;
dom (f2 | (Seg i)) = (dom f2) /\ (Seg i) by RELAT_1:61;
then A28: j in dom (f2 | (Seg i)) by A27, A26, XBOOLE_0:def 4;
thus ((f1 ^ f2) | (Seg ((len f1) + i))) . k = (f1 ^ f2) . k by A19, FUNCT_1:47
.= f2 . j by A26, FINSEQ_1:def 7
.= (f2 | (Seg i)) . j by A28, FUNCT_1:47
.= (f1 ^ (f2 | (Seg i))) . k by A24, A28, FINSEQ_1:def 7 ; :: thesis: verum

end;

end;

end;

f1 ^ (f2 | (Seg i)) c= f1 ^ f2 by Th13, RELAT_1:59;
then dom (f1 ^ (f2 | (Seg i))) c= dom (f1 ^ f2) by RELAT_1:11;
then dom (f1 ^ (f2 | (Seg i))) c= (dom (f1 ^ f2)) /\ (Seg ((len f1) + i)) by A1, XBOOLE_1:19;
then dom ((f1 ^ f2) | (Seg ((len f1) + i))) = dom (f1 ^ (f2 | (Seg i))) by A17, A9;
hence (f1 ^ f2) | (Seg ((len f1) + i)) = f1 ^ (f2 | (Seg i)) by A18, FINSEQ_1:13; :: thesis: verum