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 ;
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 ;
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 ;
dom (f2 | (Seg i)) = (dom f2) /\ (Seg i) by RELAT_1:61;
then k in Seg i by ;
then k <= i by FINSEQ_1:1;
then A8: j <= (len f1) + i by ;
1 <= k by ;
then 1 <= j by ;
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 ;
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 ;
A16: dom (f2 | (Seg i)) = (dom f2) /\ (Seg i) by RELAT_1:61;
j in Seg ((len f1) + i) by ;
then j <= (len f1) + i by FINSEQ_1:1;
then k <= i by ;
then k in Seg i by A15;
then k in dom (f2 | (Seg i)) by ;
hence x in dom (f1 ^ (f2 | (Seg i))) by ; :: 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))) . b1 = (f1 ^ (f2 | (Seg i))) . b1 )
assume A19: k in dom ((f1 ^ f2) | (Seg ((len f1) + i))) ; :: thesis: ((f1 ^ f2) | (Seg ((len f1) + i))) . b1 = (f1 ^ (f2 | (Seg i))) . b1
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))) . b1 = (f1 ^ (f2 | (Seg i))) . b1
then A21: k in dom f1 by ;
thus ((f1 ^ f2) | (Seg ((len f1) + i))) . k = (f1 ^ f2) . k by
.= f1 . k by
.= (f1 ^ (f2 | (Seg i))) . k by ; :: thesis: verum
end;
suppose A22: k > len f1 ; :: thesis: ((f1 ^ f2) | (Seg ((len f1) + i))) . b1 = (f1 ^ (f2 | (Seg i))) . b1
then reconsider j = k - (len f1) as Element of NAT by INT_1:5;
j > 0 by ;
then A23: 1 <= j by NAT_1:14;
A24: k = (len f1) + j ;
A25: not k in dom f1 by ;
k in dom (f1 ^ f2) by ;
then A26: ex n being Nat st
( n in dom f2 & k = (len f1) + n ) by ;
k in Seg ((len f1) + i) by ;
then k <= (len f1) + i by FINSEQ_1:1;
then j <= i by ;
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 ;
thus ((f1 ^ f2) | (Seg ((len f1) + i))) . k = (f1 ^ f2) . k by
.= f2 . j by
.= (f2 | (Seg i)) . j by
.= (f1 ^ (f2 | (Seg i))) . k by ; :: thesis: verum
end;
end;
end;
f1 ^ (f2 | (Seg i)) c= f1 ^ f2 by ;
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 ;
then dom ((f1 ^ f2) | (Seg ((len f1) + i))) = dom (f1 ^ (f2 | (Seg i))) by ;
hence (f1 ^ f2) | (Seg ((len f1) + i)) = f1 ^ (f2 | (Seg i)) by ; :: thesis: verum