:: FINSEQ_3 semantic presentation

theorem Th1: :: FINSEQ_3:1
Seg 3 = {1,2,3}
proof end;

theorem Th2: :: FINSEQ_3:2
Seg 4 = {1,2,3,4}
proof end;

theorem Th3: :: FINSEQ_3:3
Seg 5 = {1,2,3,4,5}
proof end;

theorem Th4: :: FINSEQ_3:4
Seg 6 = {1,2,3,4,5,6}
proof end;

theorem Th5: :: FINSEQ_3:5
Seg 7 = {1,2,3,4,5,6,7}
proof end;

theorem Th6: :: FINSEQ_3:6
Seg 8 = {1,2,3,4,5,6,7,8}
proof end;

theorem Th7: :: FINSEQ_3:7
for b1 being natural number holds
( Seg b1 = {} iff not b1 in Seg b1 ) by FINSEQ_1:4, FINSEQ_1:5;

theorem Th8: :: FINSEQ_3:8
canceled;

theorem Th9: :: FINSEQ_3:9
for b1 being natural number holds not b1 + 1 in Seg b1
proof end;

theorem Th10: :: FINSEQ_3:10
for b1, b2 being natural number st b1 <> 0 holds
b1 in Seg (b1 + b2)
proof end;

theorem Th11: :: FINSEQ_3:11
for b1, b2 being natural number st b1 + b2 in Seg b1 holds
b2 = 0
proof end;

theorem Th12: :: FINSEQ_3:12
for b1, b2 being natural number st b1 < b2 holds
b1 + 1 in Seg b2
proof end;

theorem Th13: :: FINSEQ_3:13
for b1, b2, b3 being natural number st b1 in Seg b2 & b3 < b1 holds
b1 - b3 in Seg b2
proof end;

theorem Th14: :: FINSEQ_3:14
for b1, b2 being natural number holds
( b1 - b2 in Seg b1 iff b2 < b1 )
proof end;

theorem Th15: :: FINSEQ_3:15
for b1 being natural number holds Seg b1 misses {(b1 + 1)}
proof end;

theorem Th16: :: FINSEQ_3:16
for b1 being natural number holds (Seg (b1 + 1)) \ (Seg b1) = {(b1 + 1)}
proof end;

theorem Th17: :: FINSEQ_3:17
for b1 being natural number holds Seg b1 <> Seg (b1 + 1)
proof end;

theorem Th18: :: FINSEQ_3:18
for b1, b2 being natural number st Seg b1 = Seg (b1 + b2) holds
b2 = 0
proof end;

theorem Th19: :: FINSEQ_3:19
for b1, b2 being natural number holds Seg b1 c= Seg (b1 + b2)
proof end;

theorem Th20: :: FINSEQ_3:20
for b1, b2 being natural number holds Seg b1, Seg b2 are_c=-comparable
proof end;

theorem Th21: :: FINSEQ_3:21
canceled;

theorem Th22: :: FINSEQ_3:22
for b1 being set
for b2 being natural number st Seg b2 = {b1} holds
( b2 = 1 & b1 = 1 )
proof end;

theorem Th23: :: FINSEQ_3:23
for b1, b2 being set
for b3 being natural number st Seg b3 = {b1,b2} & b1 <> b2 holds
( b3 = 2 & {b1,b2} = {1,2} )
proof end;

theorem Th24: :: FINSEQ_3:24
for b1, b2 being FinSequence
for b3 being set st b3 in dom b1 holds
b3 in dom (b1 ^ b2)
proof end;

theorem Th25: :: FINSEQ_3:25
for b1 being FinSequence
for b2 being set st b2 in dom b1 holds
b2 is Nat
proof end;

theorem Th26: :: FINSEQ_3:26
for b1 being FinSequence
for b2 being set st b2 in dom b1 holds
b2 <> 0
proof end;

theorem Th27: :: FINSEQ_3:27
for b1 being FinSequence
for b2 being natural number holds
( b2 in dom b1 iff ( 1 <= b2 & b2 <= len b1 ) )
proof end;

theorem Th28: :: FINSEQ_3:28
for b1 being FinSequence
for b2 being natural number holds
( b2 in dom b1 iff ( b2 - 1 is Nat & (len b1) - b2 is Nat ) )
proof end;

theorem Th29: :: FINSEQ_3:29
for b1, b2 being set holds dom <*b1,b2*> = Seg 2
proof end;

theorem Th30: :: FINSEQ_3:30
for b1, b2, b3 being set holds dom <*b1,b2,b3*> = Seg 3
proof end;

theorem Th31: :: FINSEQ_3:31
for b1, b2 being FinSequence holds
( len b1 = len b2 iff dom b1 = dom b2 )
proof end;

theorem Th32: :: FINSEQ_3:32
for b1, b2 being FinSequence holds
( len b1 <= len b2 iff dom b1 c= dom b2 )
proof end;

theorem Th33: :: FINSEQ_3:33
for b1 being FinSequence
for b2 being set st b2 in rng b1 holds
1 in dom b1
proof end;

theorem Th34: :: FINSEQ_3:34
for b1 being FinSequence st rng b1 <> {} holds
1 in dom b1
proof end;

theorem Th35: :: FINSEQ_3:35
canceled;

theorem Th36: :: FINSEQ_3:36
canceled;

theorem Th37: :: FINSEQ_3:37
canceled;

theorem Th38: :: FINSEQ_3:38
for b1, b2 being set holds {} <> <*b1,b2*>
proof end;

theorem Th39: :: FINSEQ_3:39
for b1, b2, b3 being set holds {} <> <*b1,b2,b3*>
proof end;

theorem Th40: :: FINSEQ_3:40
for b1, b2, b3 being set holds <*b1*> <> <*b2,b3*>
proof end;

theorem Th41: :: FINSEQ_3:41
for b1, b2, b3, b4 being set holds <*b1*> <> <*b2,b3,b4*>
proof end;

theorem Th42: :: FINSEQ_3:42
for b1, b2, b3, b4, b5 being set holds <*b1,b2*> <> <*b3,b4,b5*>
proof end;

theorem Th43: :: FINSEQ_3:43
for b1, b2, b3 being FinSequence st len b1 = (len b2) + (len b3) & ( for b4 being Nat st b4 in dom b2 holds
b1 . b4 = b2 . b4 ) & ( for b4 being Nat st b4 in dom b3 holds
b1 . ((len b2) + b4) = b3 . b4 ) holds
b1 = b2 ^ b3
proof end;

Lemma23: for b1 being set
for b2 being natural number st b1 c= Seg b2 holds
Sgm b1 is one-to-one
proof end;

theorem Th44: :: FINSEQ_3:44
for b1 being natural number
for b2 being finite set st b2 c= Seg b1 holds
len (Sgm b2) = card b2
proof end;

theorem Th45: :: FINSEQ_3:45
for b1 being natural number
for b2 being finite set st b2 c= Seg b1 holds
dom (Sgm b2) = Seg (card b2)
proof end;

theorem Th46: :: FINSEQ_3:46
for b1 being set
for b2, b3, b4, b5, b6 being natural number st b1 c= Seg b2 & b3 < b4 & 1 <= b5 & b6 <= len (Sgm b1) & (Sgm b1) . b6 = b3 & (Sgm b1) . b5 = b4 holds
b6 < b5
proof end;

theorem Th47: :: FINSEQ_3:47
canceled;

theorem Th48: :: FINSEQ_3:48
for b1, b2 being set
for b3, b4 being natural number st b1 c= Seg b3 & b2 c= Seg b4 holds
( ( for b5, b6 being Nat st b5 in b1 & b6 in b2 holds
b5 < b6 ) iff Sgm (b1 \/ b2) = (Sgm b1) ^ (Sgm b2) )
proof end;

theorem Th49: :: FINSEQ_3:49
Sgm {} = {}
proof end;

theorem Th50: :: FINSEQ_3:50
for b1 being natural number st 0 <> b1 holds
Sgm {b1} = <*b1*>
proof end;

theorem Th51: :: FINSEQ_3:51
for b1, b2 being natural number st 0 < b1 & b1 < b2 holds
Sgm {b1,b2} = <*b1,b2*>
proof end;

theorem Th52: :: FINSEQ_3:52
for b1 being natural number holds len (Sgm (Seg b1)) = b1
proof end;

Lemma29: for b1 being natural number holds (Sgm (Seg (b1 + 0))) | (Seg b1) = Sgm (Seg b1)
proof end;

E30: now
let c1 be natural number ;
assume E31: for b1 being natural number holds (Sgm (Seg (b1 + c1))) | (Seg b1) = Sgm (Seg b1) ;
let c2 be natural number ;
set c3 = Sgm (Seg (c2 + (c1 + 1)));
set c4 = Sgm (Seg (c2 + 1));
Sgm (Seg (c2 + (c1 + 1))) = Sgm (Seg ((c2 + 1) + c1)) ;
then E32: (Sgm (Seg (c2 + (c1 + 1)))) | (Seg (c2 + 1)) = Sgm (Seg (c2 + 1)) by E31;
(Sgm (Seg (c2 + 1))) | (Seg c2) = Sgm (Seg c2)
proof
reconsider c5 = (Sgm (Seg (c2 + 1))) | (Seg c2) as FinSequence of NAT by FINSEQ_1:23;
E33: rng (Sgm (Seg (c2 + 1))) = Seg (c2 + 1) by FINSEQ_1:def 13;
E34: Sgm (Seg (c2 + 1)) is one-to-one by Lemma23;
E35: len (Sgm (Seg (c2 + 1))) = c2 + 1 by Th52;
then E36: ( dom (Sgm (Seg (c2 + 1))) = Seg (c2 + 1) & c2 <= c2 + 1 ) by FINSEQ_1:def 3, NAT_1:37;
then E37: dom c5 = Seg c2 by E35, FINSEQ_1:21;
E38: (Sgm (Seg (c2 + 1))) . (c2 + 1) = c2 + 1
proof
assume E39: not (Sgm (Seg (c2 + 1))) . (c2 + 1) = c2 + 1 ;
c2 + 1 in dom (Sgm (Seg (c2 + 1))) by E36, FINSEQ_1:6;
then ( (Sgm (Seg (c2 + 1))) . (c2 + 1) in Seg (c2 + 1) & not (Sgm (Seg (c2 + 1))) . (c2 + 1) in {(c2 + 1)} ) by E33, E39, FUNCT_1:def 5, TARSKI:def 1;
then (Sgm (Seg (c2 + 1))) . (c2 + 1) in (Seg (c2 + 1)) \ {(c2 + 1)} by XBOOLE_0:def 4;
then E40: (Sgm (Seg (c2 + 1))) . (c2 + 1) in Seg c2 by FINSEQ_1:12;
then reconsider c6 = (Sgm (Seg (c2 + 1))) . (c2 + 1) as Nat ;
c2 + 1 in rng (Sgm (Seg (c2 + 1))) by E33, FINSEQ_1:6;
then consider c7 being set such that
E41: c7 in dom (Sgm (Seg (c2 + 1))) and
E42: (Sgm (Seg (c2 + 1))) . c7 = c2 + 1 by FUNCT_1:def 5;
reconsider c8 = c7 as Nat by E41;
E43: ( 1 <= c8 & c8 <= c2 + 1 ) by E35, E41, Th27;
now
assume c8 = c2 + 1 ;
then ( c6 = c2 + 1 & c6 <= c2 & c2 < c2 + 1 ) by E40, E42, FINSEQ_1:3, XREAL_1:31;
hence contradiction ;
end;
then c8 < c2 + 1 by E43, REAL_1:def 5;
then ( c2 + 1 < c6 & c6 <= c2 & c2 < c2 + 1 ) by E35, E40, E42, E43, FINSEQ_1:3, FINSEQ_1:def 13, XREAL_1:31;
hence contradiction by XREAL_1:2;
end;
rng c5 = (rng (Sgm (Seg (c2 + 1)))) \ {((Sgm (Seg (c2 + 1))) . (c2 + 1))}
proof
thus rng c5 c= (rng (Sgm (Seg (c2 + 1)))) \ {((Sgm (Seg (c2 + 1))) . (c2 + 1))} :: according to XBOOLE_0:def 10
proof
let c6 be set ; :: according to TARSKI:def 3
assume E39: c6 in rng c5 ;
E40: rng c5 c= rng (Sgm (Seg (c2 + 1))) by FUNCT_1:76;
now
assume E41: c6 in {(c2 + 1)} ;
consider c7 being set such that
E42: c7 in dom c5 and
E43: c5 . c7 = c6 by E39, FUNCT_1:def 5;
reconsider c8 = c7 as Nat by E42;
Seg c2 c= Seg (c2 + 1) by Th19;
then E44: ( c8 in dom (Sgm (Seg (c2 + 1))) & (Sgm (Seg (c2 + 1))) . c8 = c5 . c8 & c6 = c2 + 1 & c2 + 1 in dom (Sgm (Seg (c2 + 1))) ) by E36, E37, E41, E42, FINSEQ_1:6, FUNCT_1:70, TARSKI:def 1;
( c8 <= c2 & c2 < c2 + 1 ) by E37, E42, FINSEQ_1:3, XREAL_1:31;
hence contradiction by E34, E38, E43, E44, FUNCT_1:def 8;
end;
hence c6 in (rng (Sgm (Seg (c2 + 1)))) \ {((Sgm (Seg (c2 + 1))) . (c2 + 1))} by E38, E39, E40, XBOOLE_0:def 4;
end;
let c6 be set ; :: according to TARSKI:def 3
assume E39: c6 in (rng (Sgm (Seg (c2 + 1)))) \ {((Sgm (Seg (c2 + 1))) . (c2 + 1))} ;
then c6 in rng (Sgm (Seg (c2 + 1))) by XBOOLE_0:def 4;
then consider c7 being set such that
E40: c7 in dom (Sgm (Seg (c2 + 1))) and
E41: (Sgm (Seg (c2 + 1))) . c7 = c6 by FUNCT_1:def 5;
now
assume c7 in {(c2 + 1)} ;
then ( c6 = c2 + 1 & not c6 in {(c2 + 1)} ) by E38, E39, E41, TARSKI:def 1, XBOOLE_0:def 4;
hence contradiction by TARSKI:def 1;
end;
then c7 in (Seg (c2 + 1)) \ {(c2 + 1)} by E36, E40, XBOOLE_0:def 4;
then E42: c7 in dom c5 by E37, FINSEQ_1:12;
then c5 . c7 = (Sgm (Seg (c2 + 1))) . c7 by FUNCT_1:70;
hence c6 in rng c5 by E41, E42, FUNCT_1:def 5;
end;
then E39: rng c5 = Seg c2 by E33, E38, FINSEQ_1:12;
now
let c6, c7, c8, c9 be natural number ;
assume that
E40: ( 1 <= c6 & c6 < c7 & c7 <= len c5 ) and
E41: ( c8 = c5 . c6 & c9 = c5 . c7 ) ;
E42: ( len c5 = c2 & c6 <= len c5 & 1 <= c7 ) by E35, E36, E40, XREAL_1:2, FINSEQ_1:21;
then ( c6 in dom c5 & c7 in dom c5 & len (Sgm (Seg (c2 + 1))) = c2 + 1 & c2 <= c2 + 1 ) by E37, E40, Th52, FINSEQ_1:3, NAT_1:37;
then ( c5 . c6 = (Sgm (Seg (c2 + 1))) . c6 & c5 . c7 = (Sgm (Seg (c2 + 1))) . c7 & c7 <= len (Sgm (Seg (c2 + 1))) ) by E40, E42, XREAL_1:2, FUNCT_1:70;
hence c8 < c9 by E40, E41, FINSEQ_1:def 13;
end;
hence (Sgm (Seg (c2 + 1))) | (Seg c2) = Sgm (Seg c2) by E39, FINSEQ_1:def 13;
end;
then ( Sgm (Seg c2) = (Sgm (Seg (c2 + (c1 + 1)))) | ((Seg (c2 + 1)) /\ (Seg c2)) & c2 <= c2 + 1 ) by E32, NAT_1:37, RELAT_1:100;
hence (Sgm (Seg (c2 + (c1 + 1)))) | (Seg c2) = Sgm (Seg c2) by FINSEQ_1:9;
end;

Lemma31: for b1, b2 being natural number holds (Sgm (Seg (b2 + b1))) | (Seg b2) = Sgm (Seg b2)
proof end;

theorem Th53: :: FINSEQ_3:53
for b1, b2 being natural number holds (Sgm (Seg (b1 + b2))) | (Seg b1) = Sgm (Seg b1) by Lemma31;

E32: now
let c1 be Nat;
assume E33: Sgm (Seg c1) = idseq c1 ;
E34: len (idseq (c1 + 1)) = c1 + 1 by FINSEQ_2:55;
then E35: len (Sgm (Seg (c1 + 1))) = len (idseq (c1 + 1)) by Th52;
now
let c2 be Nat;
assume E36: c2 in Seg (c1 + 1) ;
then E37: c2 in (Seg c1) \/ {(c1 + 1)} by FINSEQ_1:11;
now
per cases ( c2 in Seg c1 or c2 in {(c1 + 1)} ) by E37, XBOOLE_0:def 2;
suppose E38: c2 in Seg c1 ;
then ( (Sgm (Seg c1)) . c2 = c2 & (idseq c1) . c2 = c2 & (idseq (c1 + 1)) . c2 = c2 & (Sgm (Seg (c1 + 1))) | (Seg c1) = Sgm (Seg c1) & dom (Sgm (Seg (c1 + 1))) = Seg (c1 + 1) ) by E33, E34, E35, E36, Lemma31, FINSEQ_1:def 3, FINSEQ_2:56;
hence (Sgm (Seg (c1 + 1))) . c2 = (idseq (c1 + 1)) . c2 by E38, FUNCT_1:72;
end;
suppose c2 in {(c1 + 1)} ;
then E38: c2 = c1 + 1 by TARSKI:def 1;
then E39: c2 in Seg (c1 + 1) by FINSEQ_1:6;
set c3 = Sgm (Seg (c1 + 1));
set c4 = Sgm (Seg c1);
now
assume (Sgm (Seg (c1 + 1))) . c2 <> c2 ;
then E40: ( not (Sgm (Seg (c1 + 1))) . c2 in {c2} & Seg (c1 + 1) c= Seg (c1 + 1) ) by TARSKI:def 1;
E41: ( rng (Sgm (Seg (c1 + 1))) = Seg (c1 + 1) & dom (Sgm (Seg (c1 + 1))) = Seg (c1 + 1) ) by E34, E35, FINSEQ_1:def 3, FINSEQ_1:def 13;
then E42: (Sgm (Seg (c1 + 1))) . c2 in Seg (c1 + 1) by E36, FUNCT_1:def 5;
then (Sgm (Seg (c1 + 1))) . c2 in (Seg (c1 + 1)) \ {(c1 + 1)} by E38, E40, XBOOLE_0:def 4;
then E43: (Sgm (Seg (c1 + 1))) . c2 in Seg c1 by FINSEQ_1:12;
then reconsider c5 = (Sgm (Seg (c1 + 1))) . c2 as Nat ;
E44: Sgm (Seg (c1 + 1)) is one-to-one by Lemma23;
(Sgm (Seg (c1 + 1))) | (Seg c1) = Sgm (Seg c1) by Lemma31;
then E45: (Sgm (Seg (c1 + 1))) . c5 = (Sgm (Seg c1)) . c5 by E43, FUNCT_1:72
.= c5 by E33, E43, FINSEQ_2:56 ;
( c5 <= c1 & c1 < c1 + 1 ) by E43, FINSEQ_1:3, XREAL_1:31;
hence contradiction by E38, E39, E41, E42, E44, E45, FUNCT_1:def 8;
end;
hence (Sgm (Seg (c1 + 1))) . c2 = (idseq (c1 + 1)) . c2 by E39, FINSEQ_2:56;
end;
end;
end;
hence (Sgm (Seg (c1 + 1))) . c2 = (idseq (c1 + 1)) . c2 ;
end;
hence Sgm (Seg (c1 + 1)) = idseq (c1 + 1) by E34, E35, FINSEQ_2:10;
end;

theorem Th54: :: FINSEQ_3:54
for b1 being natural number holds Sgm (Seg b1) = idseq b1
proof end;

theorem Th55: :: FINSEQ_3:55
for b1 being FinSequence
for b2 being natural number holds
( b1 | (Seg b2) = b1 iff len b1 <= b2 )
proof end;

theorem Th56: :: FINSEQ_3:56
for b1, b2 being natural number holds (idseq (b1 + b2)) | (Seg b1) = idseq b1
proof end;

theorem Th57: :: FINSEQ_3:57
for b1, b2 being natural number holds
( (idseq b1) | (Seg b2) = idseq b2 iff b2 <= b1 )
proof end;

theorem Th58: :: FINSEQ_3:58
for b1, b2 being natural number holds
( (idseq b1) | (Seg b2) = idseq b1 iff b1 <= b2 )
proof end;

theorem Th59: :: FINSEQ_3:59
for b1, b2 being FinSequence
for b3, b4 being natural number st len b1 = b3 + b4 & b2 = b1 | (Seg b3) holds
len b2 = b3
proof end;

theorem Th60: :: FINSEQ_3:60
for b1, b2 being FinSequence
for b3, b4 being natural number st len b1 = b3 + b4 & b2 = b1 | (Seg b3) holds
dom b2 = Seg b3
proof end;

theorem Th61: :: FINSEQ_3:61
for b1, b2 being FinSequence
for b3 being natural number st len b1 = b3 + 1 & b2 = b1 | (Seg b3) holds
b1 = b2 ^ <*(b1 . (b3 + 1))*>
proof end;

theorem Th62: :: FINSEQ_3:62
for b1 being FinSequence
for b2 being set holds
( b1 | b2 is FinSequence iff ex b3 being Nat st b2 /\ (dom b1) = Seg b3 )
proof end;

theorem Th63: :: FINSEQ_3:63
for b1, b2 being FinSequence
for b3 being set holds card ((b1 ^ b2) " b3) = (card (b1 " b3)) + (card (b2 " b3))
proof end;

theorem Th64: :: FINSEQ_3:64
for b1, b2 being FinSequence
for b3 being set holds b1 " b3 c= (b1 ^ b2) " b3
proof end;

definition
let c1 be FinSequence;
let c2 be set ;
func c1 - c2 -> FinSequence equals :: FINSEQ_3:def 1
a1 * (Sgm ((dom a1) \ (a1 " a2)));
coherence
c1 * (Sgm ((dom c1) \ (c1 " c2))) is FinSequence
proof end;
end;

:: deftheorem Def1 defines - FINSEQ_3:def 1 :
for b1 being FinSequence
for b2 being set holds b1 - b2 = b1 * (Sgm ((dom b1) \ (b1 " b2)));

theorem Th65: :: FINSEQ_3:65
canceled;

theorem Th66: :: FINSEQ_3:66
for b1 being FinSequence
for b2 being set holds len (b1 - b2) = (len b1) - (card (b1 " b2))
proof end;

theorem Th67: :: FINSEQ_3:67
for b1 being FinSequence
for b2 being set holds len (b1 - b2) <= len b1
proof end;

theorem Th68: :: FINSEQ_3:68
for b1 being FinSequence
for b2 being set st len (b1 - b2) = len b1 holds
b2 misses rng b1
proof end;

theorem Th69: :: FINSEQ_3:69
for b1 being FinSequence
for b2 being set
for b3 being natural number st b3 = (len b1) - (card (b1 " b2)) holds
dom (b1 - b2) = Seg b3
proof end;

theorem Th70: :: FINSEQ_3:70
for b1 being FinSequence
for b2 being set holds dom (b1 - b2) c= dom b1
proof end;

theorem Th71: :: FINSEQ_3:71
for b1 being FinSequence
for b2 being set st dom (b1 - b2) = dom b1 holds
b2 misses rng b1
proof end;

theorem Th72: :: FINSEQ_3:72
for b1 being FinSequence
for b2 being set holds rng (b1 - b2) = (rng b1) \ b2
proof end;

theorem Th73: :: FINSEQ_3:73
for b1 being FinSequence
for b2 being set holds rng (b1 - b2) c= rng b1
proof end;

theorem Th74: :: FINSEQ_3:74
for b1 being FinSequence
for b2 being set st rng (b1 - b2) = rng b1 holds
b2 misses rng b1
proof end;

theorem Th75: :: FINSEQ_3:75
for b1 being FinSequence
for b2 being set holds
( b1 - b2 = {} iff rng b1 c= b2 )
proof end;

theorem Th76: :: FINSEQ_3:76
for b1 being FinSequence
for b2 being set holds
( b1 - b2 = b1 iff b2 misses rng b1 )
proof end;

theorem Th77: :: FINSEQ_3:77
for b1 being FinSequence
for b2 being set holds
( b1 - {b2} = b1 iff not b2 in rng b1 )
proof end;

theorem Th78: :: FINSEQ_3:78
for b1 being FinSequence holds b1 - {} = b1
proof end;

theorem Th79: :: FINSEQ_3:79
for b1 being FinSequence holds b1 - (rng b1) = {} by Th75;

Lemma46: for b1 being set holds {} - b1 = {}
proof end;

Lemma47: for b1, b2 being set holds
( <*b1*> - b2 = <*b1*> iff not b1 in b2 )
proof end;

Lemma48: for b1, b2 being set holds
( <*b1*> - b2 = {} iff b1 in b2 )
proof end;

Lemma49: for b1 being FinSequence
for b2 being set holds (b1 ^ {} ) - b2 = (b1 - b2) ^ ({} - b2)
proof end;

Lemma50: for b1 being FinSequence
for b2, b3 being set holds (b1 ^ <*b2*>) - b3 = (b1 - b3) ^ (<*b2*> - b3)
proof end;

E51: now
let c1 be FinSequence;
let c2 be set ;
assume E52: for b1 being FinSequence
for b2 being set holds (b1 ^ c1) - b2 = (b1 - b2) ^ (c1 - b2) ;
let c3 be FinSequence;
let c4 be set ;
thus (c3 ^ (c1 ^ <*c2*>)) - c4 = ((c3 ^ c1) ^ <*c2*>) - c4 by FINSEQ_1:45
.= ((c3 ^ c1) - c4) ^ (<*c2*> - c4) by Lemma50
.= ((c3 - c4) ^ (c1 - c4)) ^ (<*c2*> - c4) by E52
.= (c3 - c4) ^ ((c1 - c4) ^ (<*c2*> - c4)) by FINSEQ_1:45
.= (c3 - c4) ^ ((c1 ^ <*c2*>) - c4) by Lemma50 ;
end;

Lemma52: for b1, b2 being FinSequence
for b3 being set holds (b2 ^ b1) - b3 = (b2 - b3) ^ (b1 - b3)
proof end;

theorem Th80: :: FINSEQ_3:80
for b1, b2 being FinSequence
for b3 being set holds (b1 ^ b2) - b3 = (b1 - b3) ^ (b2 - b3) by Lemma52;

theorem Th81: :: FINSEQ_3:81
for b1 being set holds {} - b1 = {} by Lemma46;

theorem Th82: :: FINSEQ_3:82
for b1, b2 being set holds
( <*b1*> - b2 = <*b1*> iff not b1 in b2 ) by Lemma47;

theorem Th83: :: FINSEQ_3:83
for b1, b2 being set holds
( <*b1*> - b2 = {} iff b1 in b2 ) by Lemma48;

theorem Th84: :: FINSEQ_3:84
for b1, b2, b3 being set holds
( <*b1,b2*> - b3 = {} iff ( b1 in b3 & b2 in b3 ) )
proof end;

theorem Th85: :: FINSEQ_3:85
for b1, b2, b3 being set st b1 in b2 & not b3 in b2 holds
<*b1,b3*> - b2 = <*b3*>
proof end;

theorem Th86: :: FINSEQ_3:86
for b1, b2, b3 being set st <*b1,b2*> - b3 = <*b2*> & b1 <> b2 holds
( b1 in b3 & not b2 in b3 )
proof end;

theorem Th87: :: FINSEQ_3:87
for b1, b2, b3 being set st not b1 in b2 & b3 in b2 holds
<*b1,b3*> - b2 = <*b1*>
proof end;

theorem Th88: :: FINSEQ_3:88
for b1, b2, b3 being set st <*b1,b2*> - b3 = <*b1*> & b1 <> b2 holds
( not b1 in b3 & b2 in b3 )
proof end;

theorem Th89: :: FINSEQ_3:89
for b1, b2, b3 being set holds
( <*b1,b2*> - b3 = <*b1,b2*> iff ( not b1 in b3 & not b2 in b3 ) )
proof end;

theorem Th90: :: FINSEQ_3:90
for b1, b2 being FinSequence
for b3 being set
for b4 being natural number st len b1 = b4 + 1 & b2 = b1 | (Seg b4) holds
( b1 . (b4 + 1) in b3 iff b1 - b3 = b2 - b3 )
proof end;

theorem Th91: :: FINSEQ_3:91
for b1, b2 being FinSequence
for b3 being set
for b4 being natural number st len b1 = b4 + 1 & b2 = b1 | (Seg b4) holds
( not b1 . (b4 + 1) in b3 iff b1 - b3 = (b2 - b3) ^ <*(b1 . (b4 + 1))*> )
proof end;

Lemma58: for b1 being FinSequence
for b2 being set st len b1 = 0 holds
for b3 being natural number st b3 in dom b1 holds
for b4 being finite set holds
( not b4 = { b5 where B is Nat : ( b5 in dom b1 & b5 <= b3 & b1 . b5 in b2 ) } or b1 . b3 in b2 or (b1 - b2) . (b3 - (card b4)) = b1 . b3 )
proof end;

Lemma59: for b1 being natural number st ( for b2 being FinSequence
for b3 being set st len b2 = b1 holds
for b4 being natural number st b4 in dom b2 holds
for b5 being finite set holds
( not b5 = { b6 where B is Nat : ( b6 in dom b2 & b6 <= b4 & b2 . b6 in b3 ) } or b2 . b4 in b3 or (b2 - b3) . (b4 - (card b5)) = b2 . b4 ) ) holds
for b2 being FinSequence
for b3 being set st len b2 = b1 + 1 holds
for b4 being natural number st b4 in dom b2 holds
for b5 being finite set holds
( not b5 = { b6 where B is Nat : ( b6 in dom b2 & b6 <= b4 & b2 . b6 in b3 ) } or b2 . b4 in b3 or (b2 - b3) . (b4 - (card b5)) = b2 . b4 )
proof end;

Lemma60: for b1 being natural number
for b2 being FinSequence
for b3 being set st len b2 = b1 holds
for b4 being natural number st b4 in dom b2 holds
for b5 being finite set holds
( not b5 = { b6 where B is Nat : ( b6 in dom b2 & b6 <= b4 & b2 . b6 in b3 ) } or b2 . b4 in b3 or (b2 - b3) . (b4 - (card b5)) = b2 . b4 )
proof end;

theorem Th92: :: FINSEQ_3:92
for b1 being FinSequence
for b2 being set
for b3 being natural number st b3 in dom b1 holds
for b4 being finite set holds
( not b4 = { b5 where B is Nat : ( b5 in dom b1 & b5 <= b3 & b1 . b5 in b2 ) } or b1 . b3 in b2 or (b1 - b2) . (b3 - (card b4)) = b1 . b3 )
proof end;

theorem Th93: :: FINSEQ_3:93
for b1 being FinSequence
for b2, b3 being set st b1 is FinSequence of b2 holds
b1 - b3 is FinSequence of b2
proof end;

theorem Th94: :: FINSEQ_3:94
for b1 being FinSequence
for b2 being set st b1 is one-to-one holds
b1 - b2 is one-to-one
proof end;

theorem Th95: :: FINSEQ_3:95
for b1 being FinSequence
for b2 being set st b1 is one-to-one holds
len (b1 - b2) = (len b1) - (card (b2 /\ (rng b1)))
proof end;

theorem Th96: :: FINSEQ_3:96
for b1 being FinSequence
for b2 being finite set st b1 is one-to-one & b2 c= rng b1 holds
len (b1 - b2) = (len b1) - (card b2)
proof end;

theorem Th97: :: FINSEQ_3:97
for b1 being FinSequence
for b2 being set st b1 is one-to-one & b2 in rng b1 holds
len (b1 - {b2}) = (len b1) - 1
proof end;

theorem Th98: :: FINSEQ_3:98
for b1, b2 being FinSequence holds
( ( rng b1 misses rng b2 & b1 is one-to-one & b2 is one-to-one ) iff b1 ^ b2 is one-to-one )
proof end;

theorem Th99: :: FINSEQ_3:99
for b1 being set
for b2 being natural number st b1 c= Seg b2 holds
Sgm b1 is one-to-one by Lemma23;

theorem Th100: :: FINSEQ_3:100
for b1 being natural number holds idseq b1 is one-to-one
proof end;

theorem Th101: :: FINSEQ_3:101
canceled;

theorem Th102: :: FINSEQ_3:102
for b1 being set holds <*b1*> is one-to-one
proof end;

theorem Th103: :: FINSEQ_3:103
for b1, b2 being set holds
( b1 <> b2 iff <*b1,b2*> is one-to-one )
proof end;

theorem Th104: :: FINSEQ_3:104
for b1, b2, b3 being set holds
( ( b1 <> b2 & b2 <> b3 & b3 <> b1 ) iff <*b1,b2,b3*> is one-to-one )
proof end;

theorem Th105: :: FINSEQ_3:105
for b1 being FinSequence
for b2 being set st b1 is one-to-one & rng b1 = {b2} holds
len b1 = 1
proof end;

theorem Th106: :: FINSEQ_3:106
for b1 being FinSequence
for b2 being set st b1 is one-to-one & rng b1 = {b2} holds
b1 = <*b2*>
proof end;

theorem Th107: :: FINSEQ_3:107
for b1 being FinSequence
for b2, b3 being set st b1 is one-to-one & rng b1 = {b2,b3} & b2 <> b3 holds
len b1 = 2
proof end;

theorem Th108: :: FINSEQ_3:108
for b1 being FinSequence
for b2, b3 being set st b1 is one-to-one & rng b1 = {b2,b3} & b2 <> b3 & not b1 = <*b2,b3*> holds
b1 = <*b3,b2*>
proof end;

theorem Th109: :: FINSEQ_3:109
for b1 being FinSequence
for b2, b3, b4 being set st b1 is one-to-one & rng b1 = {b2,b3,b4} & <*b2,b3,b4*> is one-to-one holds
len b1 = 3
proof end;

theorem Th110: :: FINSEQ_3:110
for b1 being FinSequence
for b2, b3, b4 being set st b1 is one-to-one & rng b1 = {b2,b3,b4} & b2 <> b3 & b3 <> b4 & b2 <> b4 holds
len b1 = 3
proof end;

theorem Th111: :: FINSEQ_3:111
for b1 being non empty set
for b2 being FinSequence of b1 st not b2 is empty holds
ex b3 being Element of b1ex b4 being FinSequence of b1 st
( b3 = b2 . 1 & b2 = <*b3*> ^ b4 )
proof end;

theorem Th112: :: FINSEQ_3:112
for b1 being natural number
for b2 being FinSequence
for b3 being set st b1 in dom b2 holds
(<*b3*> ^ b2) . (b1 + 1) = b2 . b1
proof end;

definition
let c1 be natural number ;
let c2 be FinSequence;
func Del c2,c1 -> FinSequence equals :Def2: :: FINSEQ_3:def 2
a2 * (Sgm ((dom a2) \ {a1}));
coherence
c2 * (Sgm ((dom c2) \ {c1})) is FinSequence
proof end;
end;

:: deftheorem Def2 defines Del FINSEQ_3:def 2 :
for b1 being natural number
for b2 being FinSequence holds Del b2,b1 = b2 * (Sgm ((dom b2) \ {b1}));

theorem Th113: :: FINSEQ_3:113
for b1 being natural number
for b2 being FinSequence holds
( ( b1 in dom b2 implies ex b3 being Nat st
( len b2 = b3 + 1 & len (Del b2,b1) = b3 ) ) & ( not b1 in dom b2 implies Del b2,b1 = b2 ) )
proof end;

theorem Th114: :: FINSEQ_3:114
for b1 being natural number
for b2 being non empty set
for b3 being FinSequence of b2 holds Del b3,b1 is FinSequence of b2
proof end;

theorem Th115: :: FINSEQ_3:115
for b1 being natural number
for b2 being FinSequence holds rng (Del b2,b1) c= rng b2
proof end;

theorem Th116: :: FINSEQ_3:116
for b1, b2, b3 being natural number st b1 = b2 + 1 & b3 in Seg b1 holds
len (Sgm ((Seg b1) \ {b3})) = b2
proof end;

theorem Th117: :: FINSEQ_3:117
for b1, b2, b3, b4 being Nat st b4 = b3 + 1 & b2 in Seg b4 & b1 in Seg b3 holds
( ( 1 <= b1 & b1 < b2 implies (Sgm ((Seg b4) \ {b2})) . b1 = b1 ) & ( b2 <= b1 & b1 <= b3 implies (Sgm ((Seg b4) \ {b2})) . b1 = b1 + 1 ) )
proof end;

theorem Th118: :: FINSEQ_3:118
for b1 being FinSequence
for b2, b3 being natural number st len b1 = b3 + 1 & b2 in dom b1 holds
len (Del b1,b2) = b3
proof end;

theorem Th119: :: FINSEQ_3:119
for b1 being FinSequence
for b2, b3, b4 being Nat st len b1 = b3 + 1 & b4 < b2 holds
(Del b1,b2) . b4 = b1 . b4
proof end;

theorem Th120: :: FINSEQ_3:120
for b1 being FinSequence
for b2, b3, b4 being Nat st len b1 = b3 + 1 & b2 in dom b1 & b2 <= b4 & b4 <= b3 holds
(Del b1,b2) . b4 = b1 . (b4 + 1)
proof end;

theorem Th121: :: FINSEQ_3:121
for b1 being natural number
for b2 being set
for b3 being FinSequence of b2
for b4 being Nat st b4 <= b1 holds
(b3 | b1) . b4 = b3 . b4
proof end;