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 ((len f1) + i))) = (dom (f1 ^ f2)) /\ (Seg ((len f1) + i)) by RELAT_1:90;
f1 ^ (f2 | (Seg i)) c= f1 ^ f2 by Th15, RELAT_1:88;
then A2: dom (f1 ^ (f2 | (Seg i))) c= dom (f1 ^ f2) by RELAT_1:25;
dom (f1 ^ (f2 | (Seg i))) c= Seg ((len f1) + i)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in dom (f1 ^ (f2 | (Seg i))) or x in Seg ((len f1) + i) )
assume A3: x in dom (f1 ^ (f2 | (Seg i))) ; :: thesis: x in Seg ((len f1) + i)
then reconsider j = x as Element of NAT ;

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

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

then A4: j in Seg (len f1) by FINSEQ_1:def 3;
len f1 <= (len f1) + i by NAT_1:11;
then Seg (len f1) c= Seg ((len f1) + i) by FINSEQ_1:7;
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 ;
dom (f2 | (Seg i)) = (dom f2) /\ (Seg i) by RELAT_1:90;
then k in Seg i by A5, XBOOLE_0:def 4;
then k <= i by FINSEQ_1:3;
then A7: j <= (len f1) + i by A6, XREAL_1:8;
( 1 <= k & k <= j ) by A5, A6, FINSEQ_3:27, NAT_1:11;
then 1 <= j by XXREAL_0:2;
hence x in Seg ((len f1) + i) by A7, FINSEQ_1:3; :: thesis: verum

end;

end;

end;

then A8: dom (f1 ^ (f2 | (Seg i))) c= (dom (f1 ^ f2)) /\ (Seg ((len f1) + i)) by A2, XBOOLE_1:19;
(dom (f1 ^ f2)) /\ (Seg ((len f1) + i)) c= dom (f1 ^ (f2 | (Seg i)))

proof

let x be set ; :: 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 A9: x in (dom (f1 ^ f2)) /\ (Seg ((len f1) + i)) ; :: thesis: x in dom (f1 ^ (f2 | (Seg i)))
then A10: x in dom (f1 ^ f2) by XBOOLE_0:def 4;
reconsider j = x as Element of NAT by A9;

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

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

dom f1 c= dom (f1 ^ (f2 | (Seg i))) by FINSEQ_1:39;
hence x in dom (f1 ^ (f2 | (Seg i))) by A11; :: 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
A12: k in dom f2 and
A13: j = (len f1) + k ;
j in Seg ((len f1) + i) by A9, XBOOLE_0:def 4;
then j <= (len f1) + i by FINSEQ_1:3;
then A14: k <= i by A13, XREAL_1:8;
1 <= k by A12, FINSEQ_3:27;
then A15: k in Seg i by A14, FINSEQ_1:3;
dom (f2 | (Seg i)) = (dom f2) /\ (Seg i) by RELAT_1:90;
then k in dom (f2 | (Seg i)) by A12, A15, XBOOLE_0:def 4;
hence x in dom (f1 ^ (f2 | (Seg i))) by A13, FINSEQ_1:41; :: thesis: verum

end;

end;

end;

then A16: dom ((f1 ^ f2) | (Seg ((len f1) + i))) = dom (f1 ^ (f2 | (Seg i))) by A1, A8, XBOOLE_0:def 10;

now

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 A17: k in dom ((f1 ^ f2) | (Seg ((len f1) + i))) ; :: thesis: ((f1 ^ f2) | (Seg ((len f1) + i))) . b₁ = (f1 ^ (f2 | (Seg i))) . b₁
then A18: 1 <= k by FINSEQ_3:27;

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 A19: k in dom f1 by A18, FINSEQ_3:27;
thus ((f1 ^ f2) | (Seg ((len f1) + i))) . k = (f1 ^ f2) . k by A17, FUNCT_1:70
.= f1 . k by A19, FINSEQ_1:def 7
.= (f1 ^ (f2 | (Seg i))) . k by A19, FINSEQ_1:def 7 ; :: thesis: verum

end;

suppose A20: 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:18;
A21: k = (len f1) + j ;
j > 0 by A20, XREAL_1:52;
then A22: 1 <= j by NAT_1:14;
k in Seg ((len f1) + i) by A1, A17, XBOOLE_0:def 4;
then k <= (len f1) + i by FINSEQ_1:3;
then j <= i by A21, XREAL_1:8;
then A23: j in Seg i by A22, FINSEQ_1:3;
A24: not k in dom f1 by A20, FINSEQ_3:27;
k in dom (f1 ^ f2) by A1, A17, XBOOLE_0:def 4;
then consider n being Nat such that
A25: n in dom f2 and
A26: k = (len f1) + n by A24, FINSEQ_1:38;
dom (f2 | (Seg i)) = (dom f2) /\ (Seg i) by RELAT_1:90;
then A27: j in dom (f2 | (Seg i)) by A23, A25, A26, XBOOLE_0:def 4;
thus ((f1 ^ f2) | (Seg ((len f1) + i))) . k = (f1 ^ f2) . k by A17, FUNCT_1:70
.= f2 . j by A25, A26, FINSEQ_1:def 7
.= (f2 | (Seg i)) . j by A27, FUNCT_1:70
.= (f1 ^ (f2 | (Seg i))) . k by A21, A27, FINSEQ_1:def 7 ; :: thesis: verum

end;

end;

end;

hence (f1 ^ f2) | (Seg ((len f1) + i)) = f1 ^ (f2 | (Seg i)) by A16, FINSEQ_1:17; :: thesis: verum