let p1, p2 be FinSequence; :: thesis: for q1, q2 being FinSubsequence st q1 c= p1 & q2 c= p2 holds
dom (q1 \/ ((len p1) Shift q2)) c= dom (p1 ^ p2)
let q1, q2 be FinSubsequence; :: thesis: ( q1 c= p1 & q2 c= p2 implies dom (q1 \/ ((len p1) Shift q2)) c= dom (p1 ^ p2) )
assume that
A1: q1 c= p1 and
A2: q2 c= p2 ; :: thesis: dom (q1 \/ ((len p1) Shift q2)) c= dom (p1 ^ p2)
A3: dom q1 c= dom p1 by A1, GRFUNC_1:2;
A4: dom q2 c= dom p2 by A2, GRFUNC_1:2;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom (q1 \/ ((len p1) Shift q2)) or x in dom (p1 ^ p2) )
assume x in dom (q1 \/ ((len p1) Shift q2)) ; :: thesis: x in dom (p1 ^ p2)
then A5: x in (dom q1) \/ (dom ((len p1) Shift q2)) by XTUPLE_0:23;
A6: dom (p1 ^ p2) = Seg ((len p1) + (len p2)) by FINSEQ_1:def 7;
A7: now :: thesis: ( x in dom q1 implies x in dom (p1 ^ p2) )
assume A8: x in dom q1 ; :: thesis: x in dom (p1 ^ p2)
A9: dom p1 = Seg (len p1) by FINSEQ_1:def 3;
len p1 <= (len p1) + (len p2) by INT_1:6;
then Seg (len p1) c= Seg ((len p1) + (len p2)) by FINSEQ_1:5;
hence x in dom (p1 ^ p2) by A3, A6, A8, A9; :: thesis: verum
end;
now :: thesis: ( x in dom ((len p1) Shift q2) implies x in dom (p1 ^ p2) )
assume A10: x in dom ((len p1) Shift q2) ; :: thesis: x in dom (p1 ^ p2)
A11: dom ((len p1) Shift q2) c= dom ((len p1) Shift p2)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom ((len p1) Shift q2) or x in dom ((len p1) Shift p2) )
assume A12: x in dom ((len p1) Shift q2) ; :: thesis: x in dom ((len p1) Shift p2)
A13: dom ((len p1) Shift p2) = { (k + (len p1)) where k is Nat : k in dom p2 } by VALUED_1:def 12;
dom ((len p1) Shift q2) = { (k + (len p1)) where k is Nat : k in dom q2 } by VALUED_1:def 12;
then ex k being Nat st
( x = k + (len p1) & k in dom q2 ) by A12;
hence x in dom ((len p1) Shift p2) by A4, A13; :: thesis: verum
end;
dom (p1 ^ p2) = dom (p1 \/ ((len p1) Shift p2)) by VALUED_1:49
.= (dom p1) \/ (dom ((len p1) Shift p2)) by XTUPLE_0:23 ;
then dom ((len p1) Shift p2) c= dom (p1 ^ p2) by XBOOLE_1:7;
then dom ((len p1) Shift q2) c= dom (p1 ^ p2) by A11;
hence x in dom (p1 ^ p2) by A10; :: thesis: verum
end;
hence x in dom (p1 ^ p2) by A5, A7, XBOOLE_0:def 3; :: thesis: verum