:: PRE_CIRC semantic presentation

begin

scheme :: PRE_CIRC:sch 1
FraenkelFinIm{ F1() ->  non empty finite set , F2( set ) ->  set , P1[ set ] } :
  {  F2(x) where x is Element of F1() : P1[x]  }  is finite
proof
set B =  {  F2(x) where x is Element of F1() : x in F1()  }  ;
A1:  {  F2(x) where x is Element of F1() : P1[x]  }  c=  {  F2(x) where x is Element of F1() : x in F1()  }
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  F2(x) where x is Element of F1() : P1[x]  }  or a in  {  F2(x) where x is Element of F1() : x in F1()  }  )
assume  a in  {  F2(x) where x is Element of F1() : P1[x]  }  ; ::_thesis: a in  {  F2(x) where x is Element of F1() : x in F1()  }
then  ex b being Element of F1() st
( F2(b) = a & P1[b] ) ;
hence  a in  {  F2(x) where x is Element of F1() : x in F1()  }  ; ::_thesis: verum
end;
A2: F1() is finite ;
  {  F2(x) where x is Element of F1() : x in F1()  }  is finite from FRAENKEL:sch_21(A2);
hence   {  F2(x) where x is Element of F1() : P1[x]  }  is finite by A1; ::_thesis: verum
end;

theorem :: PRE_CIRC:1
for f being Function
for x, y being set st dom f = {x} & rng f = {y} holds
f = {[x,y]}
proof
let f be Function; ::_thesis: for x, y being set st dom f = {x} & rng f = {y} holds
f = {[x,y]}
let x, y be set ; ::_thesis: ( dom f = {x} & rng f = {y} implies f = {[x,y]} )
assume  ( dom f = {x} & rng f = {y} ) ; ::_thesis: f = {[x,y]}
then  f = {x} --> y by FUNCOP_1:9;
hence  f = {[x,y]} by ZFMISC_1:29; ::_thesis: verum
end;

begin

theorem :: PRE_CIRC:2
for I being set
for MSS being ManySortedSet of I holds (MSS #) . (<*> I) = {{}}
proof
let I be set ; ::_thesis: for MSS being ManySortedSet of I holds (MSS #) . (<*> I) = {{}}
let MSS be ManySortedSet of I; ::_thesis: (MSS #) . (<*> I) = {{}}
reconsider eI = <*> I as Element of I * by FINSEQ_1:49;
thus (MSS #) . (<*> I) = product (MSS * eI) by FINSEQ_2:def_5
.= {{}} by CARD_3:10 ; ::_thesis: verum
end;


scheme :: PRE_CIRC:sch 2
MSSLambda2Part{ F1() ->  set , P1[ set ], F2( set ) ->  set , F3( set ) ->  set } :
 ex f being ManySortedSet of F1() st
for i being Element of F1() st i in F1() holds
( ( P1[i] implies f . i = F2(i) ) & ( P1[i] implies f . i = F3(i) ) )
proof
defpred S1[ set , set ] means ( ( P1[$1] implies $2 = F2($1) ) & ( P1[$1] implies $2 = F3($1) ) );
A1: now__::_thesis:_for_i_being_set_st_i_in_F1()_holds_
ex_j_being_set_st_S1[i,j]
let i be set ; ::_thesis: ( i in F1() implies ex j being set st S1[i,j] )
assume  i in F1() ; ::_thesis: ex j being set st S1[i,j]
thus  ex j being set st S1[i,j] ::_thesis: verum
proof
percases ( P1[i] or not P1[i] ) ;
supposeA2: P1[i] ; ::_thesis: ex j being set st S1[i,j]
take  F2(i) ; ::_thesis: S1[i,F2(i)]
thus  S1[i,F2(i)] by A2; ::_thesis: verum
end;
supposeA3: P1[i] ; ::_thesis: ex j being set st S1[i,j]
take  F3(i) ; ::_thesis: S1[i,F3(i)]
thus  S1[i,F3(i)] by A3; ::_thesis: verum
end;
end;
end;
end;
consider f being ManySortedSet of F1() such that
A4: for i being set st i in F1() holds
S1[i,f . i] from PBOOLE:sch_3(A1);
take  f ; ::_thesis: for i being Element of F1() st i in F1() holds
( ( P1[i] implies f . i = F2(i) ) & ( P1[i] implies f . i = F3(i) ) )
thus  for i being Element of F1() st i in F1() holds
( ( P1[i] implies f . i = F2(i) ) & ( P1[i] implies f . i = F3(i) ) ) by A4; ::_thesis: verum
end;

registration
let I be set ;
cluster Relation-like V2() I -defined Function-like total V41() for set ;
existence
 ex b1 being ManySortedSet of I st
( b1 is V2() & b1 is V41() )
proof
reconsider f = I --> {{}} as Function ;
reconsider f = f as ManySortedSet of I ;
take  f ; ::_thesis: ( f is V2() & f is V41() )
thus  f is V2() ; ::_thesis: f is V41()
thus  f is V41() ::_thesis: verum
proof
let i be set ; :: according to FINSET_1:def_5 ::_thesis: ( not i in I or f . i is finite )
assume  i in I ; ::_thesis: f . i is finite
hence  f . i is finite by FUNCOP_1:7; ::_thesis: verum
end;
end;
end;

registration
let I be set ;
let M be ManySortedSet of I;
let A be Subset of I;
clusterM | A -> A -defined total for A -defined Function;
coherence
 for b1 being A -defined Function st b1 = M | A holds
b1 is total
proof
set B = M | A;
 ( dom (M | A) = (dom M) /\ A & dom M = I ) by PARTFUN1:def_2, RELAT_1:61;
then  dom (M | A) = A by XBOOLE_1:28;
hence  for b1 being A -defined Function st b1 = M | A holds
b1 is total by PARTFUN1:def_2; ::_thesis: verum
end;
end;

registration
let I be set ;
let M be ManySortedSet of I;
let A be Subset of I;
clusterM | A ->  total ;
coherence
 M | A is total ;
end;

registration
let M be non-empty Function;
let A be set ;
clusterM | A ->  non-empty ;
coherence
 M | A is non-empty
proof
 rng (M | A) c= rng M by RELAT_1:70;
hence  not {} in rng (M | A) by RELAT_1:def_9; :: according to RELAT_1:def_9 ::_thesis: verum
end;
end;

theorem Th3: :: PRE_CIRC:3
for I being non empty set
for B being V2() ManySortedSet of I holds not union (rng B) is empty
proof
let I be non empty set ; ::_thesis: for B being V2() ManySortedSet of I holds not union (rng B) is empty
let B be V2() ManySortedSet of I; ::_thesis: not union (rng B) is empty
set i = the Element of I;
 the Element of I in I ;
then  the Element of I in dom B by PARTFUN1:def_2;
then  B . the Element of I in rng B by FUNCT_1:def_3;
hence  not union (rng B) is empty by ORDERS_1:6; ::_thesis: verum
end;

theorem Th4: :: PRE_CIRC:4
for I being set holds uncurry (I --> {}) = {}
proof
let I be set ; ::_thesis: uncurry (I --> {}) = {}
percases ( I = {} or I <> {} ) ;
suppose I = {} ; ::_thesis: uncurry (I --> {}) = {}
hence  uncurry (I --> {}) = {} by FUNCT_5:43; ::_thesis: verum
end;
suppose I <> {} ; ::_thesis: uncurry (I --> {}) = {}
then  rng (I --> {}) = {{}} by FUNCOP_1:8
.= Funcs ({},{}) by FUNCT_5:57 ;
then  dom (uncurry (I --> {})) = [:(dom (I --> {})),{}:] by FUNCT_5:26
.= {} by ZFMISC_1:90 ;
hence  uncurry (I --> {}) = {} ; ::_thesis: verum
end;
end;
end;

theorem :: PRE_CIRC:5
for I being non empty set
for A being set
for B being V2() ManySortedSet of I
for F being ManySortedFunction of I --> A,B holds dom (commute F) = A
proof
let I be non empty set ; ::_thesis: for A being set
for B being V2() ManySortedSet of I
for F being ManySortedFunction of I --> A,B holds dom (commute F) = A
let A be set ; ::_thesis: for B being V2() ManySortedSet of I
for F being ManySortedFunction of I --> A,B holds dom (commute F) = A
let B be V2() ManySortedSet of I; ::_thesis: for F being ManySortedFunction of I --> A,B holds dom (commute F) = A
let F be ManySortedFunction of I --> A,B; ::_thesis: dom (commute F) = A
A1: dom B = I by PARTFUN1:def_2;
A2: dom F = I by PARTFUN1:def_2;
percases ( A is empty or not A is empty ) ;
supposeA3: A is empty ; ::_thesis: dom (commute F) = A
 rng F c= {{}}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng F or x in {{}} )
assume  x in rng F ; ::_thesis: x in {{}}
then consider i being set  such that
A4: ( i in I & x = F . i ) by A2, FUNCT_1:def_3;
 ( (I --> A) . i = A & x is Function of ((I --> A) . i),(B . i) ) by A4, FUNCOP_1:7, PBOOLE:def_15;
then  x = {} by A3;
hence  x in {{}} by TARSKI:def_1; ::_thesis: verum
end;
then  rng F = {{}} by ZFMISC_1:33;
then A5: F = I --> {} by A2, FUNCOP_1:9;
commute F = curry' (uncurry F) by FUNCT_6:def_10
.= {} by A5, Th4, FUNCT_5:42 ;
hence  dom (commute F) = A by A3; ::_thesis: verum
end;
supposeA6: not A is empty ; ::_thesis: dom (commute F) = A
 rng F c= Funcs (A,(union (rng B)))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng F or x in Funcs (A,(union (rng B))) )
assume  x in rng F ; ::_thesis: x in Funcs (A,(union (rng B)))
then consider i being set  such that
A7: i in dom F and
A8: x = F . i by FUNCT_1:def_3;
 (I --> A) . i = A by A2, A7, FUNCOP_1:7;
then reconsider x9 = x as Function of A,(B . i) by A2, A7, A8, PBOOLE:def_15;
 B . i in rng B by A1, A2, A7, FUNCT_1:def_3;
then  ( rng x9 c= B . i & B . i c= union (rng B) ) by RELAT_1:def_19, ZFMISC_1:74;
then A9: rng x9 c= union (rng B) by XBOOLE_1:1;
 dom x9 = A by A2, A7, FUNCT_2:def_1;
hence  x in Funcs (A,(union (rng B))) by A9, FUNCT_2:def_2; ::_thesis: verum
end;
then  F in Funcs (I,(Funcs (A,(union (rng B))))) by A2, FUNCT_2:def_2;
then  commute F in Funcs (A,(Funcs (I,(union (rng B))))) by A6, FUNCT_6:55;
then A10: commute F is Function of A,(Funcs (I,(union (rng B)))) by FUNCT_2:66;
 not union (rng B) is empty by Th3;
then  not Funcs (I,(union (rng B))) is empty by FUNCT_2:8;
hence  dom (commute F) = A by A10, FUNCT_2:def_1; ::_thesis: verum
end;
end;
end;

scheme :: PRE_CIRC:sch 3
LambdaRecCorrD{ F1() ->  non empty set , F2() ->  Element of F1(), F3( Nat, Element of F1()) ->  Element of F1() } :
 ( ex f being Function of NAT,F1() st
( f . 0 = F2() & ( for i being Nat holds f . (i + 1) = F3(i,(f . i)) ) ) & ( for f1, f2 being Function of NAT,F1() st f1 . 0 = F2() & ( for i being Nat holds f1 . (i + 1) = F3(i,(f1 . i)) ) & f2 . 0 = F2() & ( for i being Nat holds f2 . (i + 1) = F3(i,(f2 . i)) ) holds
f1 = f2 ) )
proof
thus  ex f being Function of NAT,F1() st
( f . 0 = F2() & ( for i being Nat holds f . (i + 1) = F3(i,(f . i)) ) ) from NAT_1:sch_12(); ::_thesis: for f1, f2 being Function of NAT,F1() st f1 . 0 = F2() & ( for i being Nat holds f1 . (i + 1) = F3(i,(f1 . i)) ) & f2 . 0 = F2() & ( for i being Nat holds f2 . (i + 1) = F3(i,(f2 . i)) ) holds
f1 = f2
let f1, f2 be Function of NAT,F1(); ::_thesis: ( f1 . 0 = F2() & ( for i being Nat holds f1 . (i + 1) = F3(i,(f1 . i)) ) & f2 . 0 = F2() & ( for i being Nat holds f2 . (i + 1) = F3(i,(f2 . i)) ) implies f1 = f2 )
assume that
A1: f1 . 0 = F2() and
A2: for i being Nat holds f1 . (i + 1) = F3(i,(f1 . i)) and
A3: f2 . 0 = F2() and
A4: for i being Nat holds f2 . (i + 1) = F3(i,(f2 . i)) ; ::_thesis: f1 = f2
thus  f1 = f2 from NAT_1:sch_16(A1, A2, A3, A4); ::_thesis: verum
end;

scheme :: PRE_CIRC:sch 4
LambdaMSFD{ F1() ->  non empty set , F2() ->  Subset of F1(), F3() ->  ManySortedSet of F2(), F4() ->  ManySortedSet of F2(), F5( set ) ->  set } :
 ex f being ManySortedFunction of F3(),F4() st
for i being Element of F1() st i in F2() holds
f . i = F5(i)
provided
A1: for i being Element of F1() st i in F2() holds
F5(i) is Function of (F3() . i),(F4() . i)
proof
consider f being ManySortedSet of F2() such that
A2: for i being set st i in F2() holds
f . i = F5(i) from PBOOLE:sch_4();
 f is Function-yielding
proof
let i be set ; :: according to FUNCOP_1:def_6 ::_thesis: ( not i in proj1 f or f . i is set )
assume  i in dom f ; ::_thesis: f . i is set
then A3: i in F2() by PARTFUN1:def_2;
then  F5(i) is Function by A1;
hence  f . i is set by A2, A3; ::_thesis: verum
end;
then reconsider f = f as ManySortedFunction of F2() ;
 f is ManySortedFunction of F3(),F4()
proof
let i be set ; :: according to PBOOLE:def_15 ::_thesis: ( not i in F2() or f . i is Element of bool [:(F3() . i),(F4() . i):] )
assume A4: i in F2() ; ::_thesis: f . i is Element of bool [:(F3() . i),(F4() . i):]
then  F5(i) is Function of (F3() . i),(F4() . i) by A1;
hence  f . i is Element of bool [:(F3() . i),(F4() . i):] by A2, A4; ::_thesis: verum
end;
then reconsider f = f as ManySortedFunction of F3(),F4() ;
take  f ; ::_thesis: for i being Element of F1() st i in F2() holds
f . i = F5(i)
thus  for i being Element of F1() st i in F2() holds
f . i = F5(i) by A2; ::_thesis: verum
end;

theorem :: PRE_CIRC:6
for I being set
for f being V2() ManySortedSet of I
for g being Function
for s being Element of product f st dom g c= dom f & ( for x being set st x in dom g holds
g . x in f . x ) holds
s +* g is Element of product f
proof
let I be set ; ::_thesis: for f being V2() ManySortedSet of I
for g being Function
for s being Element of product f st dom g c= dom f & ( for x being set st x in dom g holds
g . x in f . x ) holds
s +* g is Element of product f
let f be V2() ManySortedSet of I; ::_thesis: for g being Function
for s being Element of product f st dom g c= dom f & ( for x being set st x in dom g holds
g . x in f . x ) holds
s +* g is Element of product f
let g be Function; ::_thesis: for s being Element of product f st dom g c= dom f & ( for x being set st x in dom g holds
g . x in f . x ) holds
s +* g is Element of product f
let s be Element of product f; ::_thesis: ( dom g c= dom f & ( for x being set st x in dom g holds
g . x in f . x ) implies s +* g is Element of product f )
assume that
A1: dom g c= dom f and
A2: for x being set st x in dom g holds
g . x in f . x ; ::_thesis: s +* g is Element of product f
A3: now__::_thesis:_for_x_being_set_st_x_in_dom_f_holds_
(s_+*_g)_._x_in_f_._x
let x be set ; ::_thesis: ( x in dom f implies (s +* g) . b1 in f . b1 )
assume A4: x in dom f ; ::_thesis: (s +* g) . b1 in f . b1
percases ( x in dom g or not x in dom g ) ;
supposeA5: x in dom g ; ::_thesis: (s +* g) . b1 in f . b1
then  (s +* g) . x = g . x by FUNCT_4:13;
hence  (s +* g) . x in f . x by A2, A5; ::_thesis: verum
end;
supposeA6: not x in dom g ; ::_thesis: (s +* g) . b1 in f . b1
A7: ex g9 being Function st
( s = g9 & dom g9 = dom f & ( for x being set st x in dom f holds
g9 . x in f . x ) ) by CARD_3:def_5;
 (s +* g) . x = s . x by A6, FUNCT_4:11;
hence  (s +* g) . x in f . x by A4, A7; ::_thesis: verum
end;
end;
end;
 ( dom (s +* g) = (dom s) \/ (dom g) & dom s = dom f ) by CARD_3:9, FUNCT_4:def_1;
then  dom (s +* g) = dom f by A1, XBOOLE_1:12;
hence  s +* g is Element of product f by A3, CARD_3:9; ::_thesis: verum
end;

theorem :: PRE_CIRC:7
for A, B being non empty set
for C being V2() ManySortedSet of A
for InpFs being ManySortedFunction of A --> B,C
for b being Element of B ex c being ManySortedSet of A st
( c = (commute InpFs) . b & c in C )
proof
let A, B be non empty set ; ::_thesis: for C being V2() ManySortedSet of A
for InpFs being ManySortedFunction of A --> B,C
for b being Element of B ex c being ManySortedSet of A st
( c = (commute InpFs) . b & c in C )
let C be V2() ManySortedSet of A; ::_thesis: for InpFs being ManySortedFunction of A --> B,C
for b being Element of B ex c being ManySortedSet of A st
( c = (commute InpFs) . b & c in C )
let InpFs be ManySortedFunction of A --> B,C; ::_thesis: for b being Element of B ex c being ManySortedSet of A st
( c = (commute InpFs) . b & c in C )
let b be Element of B; ::_thesis: ex c being ManySortedSet of A st
( c = (commute InpFs) . b & c in C )
A1: dom InpFs = A by PARTFUN1:def_2;
 dom (uncurry InpFs) = [:A,B:]
proof
thus  dom (uncurry InpFs) c= [:A,B:] :: according to XBOOLE_0:def_10 ::_thesis: [:A,B:] c= dom (uncurry InpFs)
proof
let i be set ; :: according to TARSKI:def_3 ::_thesis: ( not i in dom (uncurry InpFs) or i in [:A,B:] )
assume  i in dom (uncurry InpFs) ; ::_thesis: i in [:A,B:]
then consider x being set , g being Function, y being set  such that
A2: i = [x,y] and
A3: x in dom InpFs and
A4: g = InpFs . x and
A5: y in dom g by FUNCT_5:def_2;
 g is Function of ((A --> B) . x),(C . x) by A1, A3, A4, PBOOLE:def_15;
then  dom g = (A --> B) . x by A1, A3, FUNCT_2:def_1;
then  dom g = B by A1, A3, FUNCOP_1:7;
hence  i in [:A,B:] by A1, A2, A3, A5, ZFMISC_1:87; ::_thesis: verum
end;
let i1, i2 be set ; :: according to RELAT_1:def_3 ::_thesis: ( not [i1,i2] in [:A,B:] or [i1,i2] in dom (uncurry InpFs) )
reconsider g = InpFs . ([i1,i2] `1) as Function ;
assume A6: [i1,i2] in [:A,B:] ; ::_thesis: [i1,i2] in dom (uncurry InpFs)
then A7: [i1,i2] `1 in dom InpFs by A1, MCART_1:10;
 g is Function of ((A --> B) . ([i1,i2] `1)),(C . ([i1,i2] `1)) by A6, MCART_1:10, PBOOLE:def_15;
then  dom g = (A --> B) . ([i1,i2] `1) by A1, A7, FUNCT_2:def_1;
then  dom g = B by A6, FUNCOP_1:7, MCART_1:10;
then A8: [i1,i2] `2 in dom g by A6, MCART_1:10;
thus  [i1,i2] in dom (uncurry InpFs) by A7, A8, FUNCT_5:38; ::_thesis: verum
end;
then A9: ( commute InpFs = curry' (uncurry InpFs) & ex g being Function st
( (curry' (uncurry InpFs)) . b = g & dom g = A & rng g c= rng (uncurry InpFs) & ( for i being set st i in A holds
g . i = (uncurry InpFs) . (i,b) ) ) ) by FUNCT_5:32, FUNCT_6:def_10;
then reconsider c = (commute InpFs) . b as ManySortedSet of A by PARTFUN1:def_2, RELAT_1:def_18;
take  c ; ::_thesis: ( c = (commute InpFs) . b & c in C )
thus  c = (commute InpFs) . b ; ::_thesis: c in C
let i be set ; :: according to PBOOLE:def_1 ::_thesis: ( not i in A or c . i in C . i )
reconsider h = InpFs . i as Function ;
assume A10: i in A ; ::_thesis: c . i in C . i
then  (A --> B) . i = B by FUNCOP_1:7;
then A11: h is Function of B,(C . i) by A10, PBOOLE:def_15;
then A12: dom h = B by A10, FUNCT_2:def_1;
c . i = (uncurry InpFs) . (i,b) by A9, A10
.= h . b by A1, A10, A12, FUNCT_5:38 ;
hence  c . i in C . i by A10, A11, FUNCT_2:5; ::_thesis: verum
end;

theorem :: PRE_CIRC:8
for n being Element of NAT
for a being set holds product (n |-> {a}) = {(n |-> a)}
proof
let n be Element of NAT ; ::_thesis: for a being set holds product (n |-> {a}) = {(n |-> a)}
let a be set ; ::_thesis: product (n |-> {a}) = {(n |-> a)}
now__::_thesis:_for_i_being_set_holds_
(_(_i_in_product_(n_|->_{a})_implies_i_=_n_|->_a_)_&_(_i_=_n_|->_a_implies_i_in_product_(n_|->_{a})_)_)
let i be set ; ::_thesis: ( ( i in product (n |-> {a}) implies i = n |-> a ) & ( i = n |-> a implies i in product (n |-> {a}) ) )
hereby  ::_thesis: ( i = n |-> a implies i in product (n |-> {a}) )
assume  i in product (n |-> {a}) ; ::_thesis: i = n |-> a
then consider g being Function such that
A1: i = g and
A2: dom g = dom (n |-> {a}) and
A3: for x being set st x in dom (n |-> {a}) holds
g . x in (n |-> {a}) . x by CARD_3:def_5;
A4: dom g = Seg n by A2, FUNCOP_1:13;
now__::_thesis:_for_x_being_set_st_x_in_dom_g_holds_
g_._x_=_a
let x be set ; ::_thesis: ( x in dom g implies g . x = a )
assume A5: x in dom g ; ::_thesis: g . x = a
then  g . x in (n |-> {a}) . x by A2, A3;
then  g . x in {a} by A4, A5, FUNCOP_1:7;
hence  g . x = a by TARSKI:def_1; ::_thesis: verum
end;
hence  i = n |-> a by A1, A4, FUNCOP_1:11; ::_thesis: verum
end;
assume A6: i = n |-> a ; ::_thesis: i in product (n |-> {a})
then reconsider g = i as Function ;
A7: now__::_thesis:_for_x_being_set_st_x_in_dom_(n_|->_{a})_holds_
g_._x_in_(n_|->_{a})_._x
let x be set ; ::_thesis: ( x in dom (n |-> {a}) implies g . x in (n |-> {a}) . x )
assume  x in dom (n |-> {a}) ; ::_thesis: g . x in (n |-> {a}) . x
then  x in Seg n by FUNCOP_1:13;
then  ( g . x = a & (n |-> {a}) . x = {a} ) by A6, FUNCOP_1:7;
hence  g . x in (n |-> {a}) . x by TARSKI:def_1; ::_thesis: verum
end;
dom g = Seg n by A6, FUNCOP_1:13
.= dom (n |-> {a}) by FUNCOP_1:13 ;
hence  i in product (n |-> {a}) by A7, CARD_3:9; ::_thesis: verum
end;
hence  product (n |-> {a}) = {(n |-> a)} by TARSKI:def_1; ::_thesis: verum
end;

begin


registration
let D be non empty set ;
cluster  ->  finite for Element of FinTrees D;
coherence
 for b1 being Element of FinTrees D holds b1 is finite
proof
let t be Element of FinTrees D; ::_thesis: t is finite
 dom t is finite ;
hence  t is finite by FINSET_1:10; ::_thesis: verum
end;
end;

registration
let T be finite DecoratedTree;
let t be Element of dom T;
clusterT | t ->  finite ;
coherence
 T | t is finite
proof
 dom (T | t) = (dom T) | t by TREES_2:def_10;
hence  T | t is finite by FINSET_1:10; ::_thesis: verum
end;
end;

theorem Th9: :: PRE_CIRC:9
for T being finite Tree
for p being Element of T holds T | p, {  t where t is Element of T : p is_a_prefix_of t  }  are_equipotent
proof
let T be finite Tree; ::_thesis: for p being Element of T holds T | p, {  t where t is Element of T : p is_a_prefix_of t  }  are_equipotent
let p be Element of T; ::_thesis: T | p, {  t where t is Element of T : p is_a_prefix_of t  }  are_equipotent
set X =  {  t where t is Element of T : p is_a_prefix_of t  }  ;
deffunc H1( Element of T | p) ->  FinSequence of NAT = p ^ $1;
consider f being Function such that
A1: dom f = T | p and
A2: for n being Element of T | p holds f . n = H1(n) from FUNCT_1:sch_4();
take  f ; :: according to WELLORD2:def_4 ::_thesis: ( f is one-to-one & proj1 f = T | p & proj2 f =  {  t where t is Element of T : p is_a_prefix_of t  }  )
thus  f is one-to-one ::_thesis: ( proj1 f = T | p & proj2 f =  {  t where t is Element of T : p is_a_prefix_of t  }  )
proof
let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds
( not x in proj1 f or not b1 in proj1 f or not f . x = f . b1 or x = b1 )
let y be set ; ::_thesis: ( not x in proj1 f or not y in proj1 f or not f . x = f . y or x = y )
assume that
A3: ( x in dom f & y in dom f ) and
A4: f . x = f . y ; ::_thesis: x = y
reconsider m = x, n = y as Element of T | p by A1, A3;
p ^ m = f . n by A2, A4
.= p ^ n by A2 ;
hence  x = y by FINSEQ_1:33; ::_thesis: verum
end;
thus  dom f = T | p by A1; ::_thesis: proj2 f =  {  t where t is Element of T : p is_a_prefix_of t  }
thus  rng f c=  {  t where t is Element of T : p is_a_prefix_of t  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  t where t is Element of T : p is_a_prefix_of t  }  c= proj2 f
proof
let i be set ; :: according to TARSKI:def_3 ::_thesis: ( not i in rng f or i in  {  t where t is Element of T : p is_a_prefix_of t  }  )
assume  i in rng f ; ::_thesis: i in  {  t where t is Element of T : p is_a_prefix_of t  }
then consider n being set  such that
A5: n in dom f and
A6: i = f . n by FUNCT_1:def_3;
reconsider n = n as Element of T | p by A1, A5;
reconsider t = p ^ n as Element of T by TREES_1:def_6;
 ( f . n = p ^ n & p is_a_prefix_of t ) by A2, TREES_1:1;
hence  i in  {  t where t is Element of T : p is_a_prefix_of t  }  by A6; ::_thesis: verum
end;
let i be set ; :: according to TARSKI:def_3 ::_thesis: ( not i in  {  t where t is Element of T : p is_a_prefix_of t  }  or i in proj2 f )
assume  i in  {  t where t is Element of T : p is_a_prefix_of t  }  ; ::_thesis: i in proj2 f
then A7: ex t being Element of T st
( i = t & p is_a_prefix_of t ) ;
then consider n being FinSequence such that
A8: i = p ^ n by TREES_1:1;
 n is FinSequence of NAT by A7, A8, FINSEQ_1:36;
then reconsider n = n as Element of T | p by A7, A8, TREES_1:def_6;
 i = f . n by A2, A8;
hence  i in proj2 f by A1, FUNCT_1:def_3; ::_thesis: verum
end;

registration
let T be finite DecoratedTree-like Function;
let t be Element of dom T;
let T1 be finite DecoratedTree;
clusterT with-replacement (t,T1) ->  finite ;
coherence
 T with-replacement (t,T1) is finite
proof
 dom (T with-replacement (t,T1)) = (dom T) with-replacement (t,(dom T1)) by TREES_2:def_11;
hence  T with-replacement (t,T1) is finite by FINSET_1:10; ::_thesis: verum
end;
end;

theorem Th10: :: PRE_CIRC:10
for T, T1 being finite Tree
for p being Element of T holds T with-replacement (p,T1) =  {  t where t is Element of T : not p is_a_prefix_of t  }  \/  {  (p ^ t1) where t1 is Element of T1 : verum  }
proof
let T, T1 be finite Tree; ::_thesis: for p being Element of T holds T with-replacement (p,T1) =  {  t where t is Element of T : not p is_a_prefix_of t  }  \/  {  (p ^ t1) where t1 is Element of T1 : verum  }
let p be Element of T; ::_thesis: T with-replacement (p,T1) =  {  t where t is Element of T : not p is_a_prefix_of t  }  \/  {  (p ^ t1) where t1 is Element of T1 : verum  }
defpred S1[ set ] means verum;
defpred S2[ set ] means $1 = $1;
deffunc H1( FinSequence) ->  set = p ^ $1;
set A =  {  t where t is Element of T : not p is_a_proper_prefix_of t  }  ;
set B =  {  H1(t1) where t1 is Element of T1 : S2[t1]  }  ;
set C =  {  t where t is Element of T : not p is_a_prefix_of t  }  ;
set D =  {  H1(t1) where t1 is Element of T1 : S1[t1]  }  ;
now__::_thesis:_for_x_being_set_holds_
(_(_not_x_in__{__t_where_t_is_Element_of_T_:_not_p_is_a_proper_prefix_of_t__}__or_x_in__{__t_where_t_is_Element_of_T_:_not_p_is_a_prefix_of_t__}__or_x_in_{p}_)_&_(_(_x_in__{__t_where_t_is_Element_of_T_:_not_p_is_a_prefix_of_t__}__or_x_in_{p}_)_implies_x_in__{__t_where_t_is_Element_of_T_:_not_p_is_a_proper_prefix_of_t__}__)_)
let x be set ; ::_thesis: ( ( not x in  {  t where t is Element of T : not p is_a_proper_prefix_of t  }  or x in  {  t where t is Element of T : not p is_a_prefix_of t  }  or x in {p} ) & ( ( x in  {  t where t is Element of T : not p is_a_prefix_of t  }  or x in {p} ) implies x in  {  t where t is Element of T : not p is_a_proper_prefix_of t  }  ) )
hereby  ::_thesis: ( ( x in  {  t where t is Element of T : not p is_a_prefix_of t  }  or x in {p} ) implies x in  {  t where t is Element of T : not p is_a_proper_prefix_of t  }  )
assume  x in  {  t where t is Element of T : not p is_a_proper_prefix_of t  }  ; ::_thesis: ( x in  {  t where t is Element of T : not p is_a_prefix_of t  }  or x in {p} )
then consider t being Element of T such that
A1: x = t and
A2: not p is_a_proper_prefix_of t ;
 ( not p is_a_prefix_of t or t = p ) by A2, XBOOLE_0:def_8;
hence  ( x in  {  t where t is Element of T : not p is_a_prefix_of t  }  or x in {p} ) by A1, TARSKI:def_1; ::_thesis: verum
end;
assume  ( x in  {  t where t is Element of T : not p is_a_prefix_of t  }  or x in {p} ) ; ::_thesis: x in  {  t where t is Element of T : not p is_a_proper_prefix_of t  }
then  ( x = p or ex t being Element of T st
( t = x & not p is_a_prefix_of t ) ) by TARSKI:def_1;
then consider t being Element of T such that
A3: t = x and
A4: ( t = p or not p is_a_prefix_of t ) ;
 not p is_a_proper_prefix_of t by A4, XBOOLE_0:def_8;
hence  x in  {  t where t is Element of T : not p is_a_proper_prefix_of t  }  by A3; ::_thesis: verum
end;
then A5:  {  t where t is Element of T : not p is_a_proper_prefix_of t  }  =  {  t where t is Element of T : not p is_a_prefix_of t  }  \/ {p} by XBOOLE_0:def_3;
 ( {} is Element of T1 & p ^ {} = p ) by FINSEQ_1:34, TREES_1:22;
then A6: p in  {  H1(t1) where t1 is Element of T1 : S1[t1]  }  ;
A7: for t1 being Element of T1 holds
( S2[t1] iff S1[t1] ) ;
  {  H1(t1) where t1 is Element of T1 : S2[t1]  }  =  {  H1(t1) where t1 is Element of T1 : S1[t1]  }  from FRAENKEL:sch_3(A7);
hence T with-replacement (p,T1) = ( {  t where t is Element of T : not p is_a_prefix_of t  }  \/ {p}) \/  {  H1(t1) where t1 is Element of T1 : S1[t1]  }  by A5, TREES_1:32
.=  {  t where t is Element of T : not p is_a_prefix_of t  }  \/ ({p} \/  {  H1(t1) where t1 is Element of T1 : S1[t1]  }  ) by XBOOLE_1:4
.=  {  t where t is Element of T : not p is_a_prefix_of t  }  \/  {  H1(t1) where t1 is Element of T1 : S1[t1]  }  by A6, ZFMISC_1:40 ;
::_thesis: verum
end;

theorem Th11: :: PRE_CIRC:11
for T, T1 being finite Tree
for p being Element of T
for f being FinSequence of NAT st f in T with-replacement (p,T1) & p is_a_prefix_of f holds
ex t1 being Element of T1 st f = p ^ t1
proof
let T, T1 be finite Tree; ::_thesis: for p being Element of T
for f being FinSequence of NAT st f in T with-replacement (p,T1) & p is_a_prefix_of f holds
ex t1 being Element of T1 st f = p ^ t1
let p be Element of T; ::_thesis: for f being FinSequence of NAT st f in T with-replacement (p,T1) & p is_a_prefix_of f holds
ex t1 being Element of T1 st f = p ^ t1
let f be FinSequence of NAT ; ::_thesis: ( f in T with-replacement (p,T1) & p is_a_prefix_of f implies ex t1 being Element of T1 st f = p ^ t1 )
assume that
A1: f in T with-replacement (p,T1) and
A2: p is_a_prefix_of f ; ::_thesis: ex t1 being Element of T1 st f = p ^ t1
A3: not f in  {  t where t is Element of T : not p is_a_prefix_of t  }
proof
assume  f in  {  t where t is Element of T : not p is_a_prefix_of t  }  ; ::_thesis: contradiction
then  ex t being Element of T st
( f = t & not p is_a_prefix_of t ) ;
hence  contradiction by A2; ::_thesis: verum
end;
 T with-replacement (p,T1) =  {  t where t is Element of T : not p is_a_prefix_of t  }  \/  {  (p ^ t1) where t1 is Element of T1 : verum  }  by Th10;
then  f in  {  (p ^ t1) where t1 is Element of T1 : verum  }  by A1, A3, XBOOLE_0:def_3;
hence  ex t1 being Element of T1 st f = p ^ t1 ; ::_thesis: verum
end;

theorem Th12: :: PRE_CIRC:12
for p being Tree-yielding FinSequence
for k being Element of NAT st k + 1 in dom p holds
(tree p) | <*k*> = p . (k + 1)
proof
let p be Tree-yielding FinSequence; ::_thesis: for k being Element of NAT st k + 1 in dom p holds
(tree p) | <*k*> = p . (k + 1)
let k be Element of NAT ; ::_thesis: ( k + 1 in dom p implies (tree p) | <*k*> = p . (k + 1) )
assume  k + 1 in dom p ; ::_thesis: (tree p) | <*k*> = p . (k + 1)
then  k + 1 <= len p by FINSEQ_3:25;
then  k < len p by NAT_1:13;
hence  (tree p) | <*k*> = p . (k + 1) by TREES_3:49; ::_thesis: verum
end;

theorem :: PRE_CIRC:13
for q being DTree-yielding FinSequence
for k being Element of NAT st k + 1 in dom q holds
<*k*> in tree (doms q)
proof
let q be DTree-yielding FinSequence; ::_thesis: for k being Element of NAT st k + 1 in dom q holds
<*k*> in tree (doms q)
let k be Element of NAT ; ::_thesis: ( k + 1 in dom q implies <*k*> in tree (doms q) )
A1: k < k + 1 by XREAL_1:29;
A2: ( dom q = Seg (len q) & Seg (len (doms q)) = dom (doms q) ) by FINSEQ_1:def_3;
assume A3: k + 1 in dom q ; ::_thesis: <*k*> in tree (doms q)
then  k + 1 <= len q by FINSEQ_3:25;
then  k < len q by A1, XXREAL_0:2;
then A4: k < len (doms q) by A2, FINSEQ_1:6, TREES_3:37;
 dom (doms q) = dom q by TREES_3:37;
then  (doms q) . (k + 1) is Tree by A3, TREES_3:22;
then A5: {} in (doms q) . (k + 1) by TREES_1:22;
 <*k*> = <*k*> ^ {} by FINSEQ_1:34;
hence  <*k*> in tree (doms q) by A5, A4, TREES_3:def_15; ::_thesis: verum
end;

theorem Th14: :: PRE_CIRC:14
for p, q being Tree-yielding FinSequence
for k being Element of NAT st len p = len q & k + 1 in dom p & ( for i being Element of NAT st i in dom p & i <> k + 1 holds
p . i = q . i ) holds
for t being Tree st q . (k + 1) = t holds
tree q = (tree p) with-replacement (<*k*>,t)
proof
let p, q be Tree-yielding FinSequence; ::_thesis: for k being Element of NAT st len p = len q & k + 1 in dom p & ( for i being Element of NAT st i in dom p & i <> k + 1 holds
p . i = q . i ) holds
for t being Tree st q . (k + 1) = t holds
tree q = (tree p) with-replacement (<*k*>,t)
let k be Element of NAT ; ::_thesis: ( len p = len q & k + 1 in dom p & ( for i being Element of NAT st i in dom p & i <> k + 1 holds
p . i = q . i ) implies for t being Tree st q . (k + 1) = t holds
tree q = (tree p) with-replacement (<*k*>,t) )
assume that
A1: len p = len q and
A2: k + 1 in dom p and
A3: for i being Element of NAT st i in dom p & i <> k + 1 holds
p . i = q . i ; ::_thesis: for t being Tree st q . (k + 1) = t holds
tree q = (tree p) with-replacement (<*k*>,t)
let t be Tree; ::_thesis: ( q . (k + 1) = t implies tree q = (tree p) with-replacement (<*k*>,t) )
set o = <*k*>;
 k + 1 <= len p by A2, FINSEQ_3:25;
then A4: k < len p by NAT_1:13;
assume A5: q . (k + 1) = t ; ::_thesis: tree q = (tree p) with-replacement (<*k*>,t)
A6: now__::_thesis:_for_s_being_FinSequence_of_NAT_holds_
(_(_not_s_in_tree_q_or_(_s_in_tree_p_&_not_<*k*>_is_a_proper_prefix_of_s_)_or_ex_r_being_FinSequence_of_NAT_st_
(_r_in_t_&_s_=_<*k*>_^_r_)_)_&_(_(_(_s_in_tree_p_&_not_<*k*>_is_a_proper_prefix_of_s_)_or_ex_r_being_FinSequence_of_NAT_st_
(_r_in_t_&_s_=_<*k*>_^_r_)_)_implies_s_in_tree_q_)_)
let s be FinSequence of NAT ; ::_thesis: ( ( not s in tree q or ( s in tree p & not <*k*> is_a_proper_prefix_of s ) or ex r being FinSequence of NAT st
( r in t & s = <*k*> ^ r ) ) & ( ( ( s in tree p & not <*k*> is_a_proper_prefix_of s ) or ex r being FinSequence of NAT st
( r in t & s = <*k*> ^ r ) ) implies b1 in tree q ) )
hereby  ::_thesis: ( ( ( s in tree p & not <*k*> is_a_proper_prefix_of s ) or ex r being FinSequence of NAT st
( r in t & s = <*k*> ^ r ) ) implies b1 in tree q )
assume A7: s in tree q ; ::_thesis: ( ( s in tree p & not <*k*> is_a_proper_prefix_of s ) or ex r being FinSequence of NAT st
( r in t & s = <*k*> ^ r ) )
percases ( s = {} or ex n being Element of NAT ex r being FinSequence st
( n < len q & r in q . (n + 1) & s = <*n*> ^ r ) ) by A7, TREES_3:def_15;
suppose s = {} ; ::_thesis: ( ( s in tree p & not <*k*> is_a_proper_prefix_of s ) or ex r being FinSequence of NAT st
( r in t & s = <*k*> ^ r ) )
hence  ( ( s in tree p & not <*k*> is_a_proper_prefix_of s ) or ex r being FinSequence of NAT st
( r in t & s = <*k*> ^ r ) ) by TREES_1:22, XBOOLE_1:115; ::_thesis: verum
end;
suppose ex n being Element of NAT ex r being FinSequence st
( n < len q & r in q . (n + 1) & s = <*n*> ^ r ) ; ::_thesis: ( ( s in tree p & not <*k*> is_a_proper_prefix_of s ) or ex r being FinSequence of NAT st
( r in t & s = <*k*> ^ r ) )
then consider n being Element of NAT , r being FinSequence such that
A8: n < len q and
A9: r in q . (n + 1) and
A10: s = <*n*> ^ r ;
now__::_thesis:_(_(_n_=_k_&_ex_r_being_FinSequence_of_NAT_st_
(_r_in_t_&_s_=_<*k*>_^_r_)_)_or_(_n_<>_k_&_s_in_tree_p_&_not_<*k*>_is_a_proper_prefix_of_s_)_)
percases ( n = k or n <> k ) ;
caseA11: n = k ; ::_thesis: ex r being FinSequence of NAT st
( r in t & s = <*k*> ^ r )
reconsider r = r as FinSequence of NAT by A10, FINSEQ_1:36;
take r = r; ::_thesis: ( r in t & s = <*k*> ^ r )
thus  ( r in t & s = <*k*> ^ r ) by A5, A9, A10, A11; ::_thesis: verum
end;
caseA12: n <> k ; ::_thesis: ( s in tree p & not <*k*> is_a_proper_prefix_of s )
 ( 1 <= n + 1 & n + 1 <= len p ) by A1, A8, NAT_1:11, NAT_1:13;
then  n + 1 in dom p by FINSEQ_3:25;
then  q . (n + 1) = p . (n + 1) by A3, A12, XCMPLX_1:2;
hence  s in tree p by A1, A8, A9, A10, TREES_3:def_15; ::_thesis: not <*k*> is_a_proper_prefix_of s
assume  <*k*> is_a_proper_prefix_of s ; ::_thesis: contradiction
then  <*k*> is_a_prefix_of s by XBOOLE_0:def_8;
then  ex s1 being FinSequence st s = <*k*> ^ s1 by TREES_1:1;
then k = s . 1 by FINSEQ_1:41
.= n by A10, FINSEQ_1:41 ;
hence  contradiction by A12; ::_thesis: verum
end;
end;
end;
hence  ( ( s in tree p & not <*k*> is_a_proper_prefix_of s ) or ex r being FinSequence of NAT st
( r in t & s = <*k*> ^ r ) ) ; ::_thesis: verum
end;
end;
end;
assume A13: ( ( s in tree p & not <*k*> is_a_proper_prefix_of s ) or ex r being FinSequence of NAT st
( r in t & s = <*k*> ^ r ) ) ; ::_thesis: b1 in tree q
percases ( ( s in tree p & not <*k*> is_a_proper_prefix_of s ) or ex r being FinSequence of NAT st
( r in t & s = <*k*> ^ r ) ) by A13;
supposethat A14: s in tree p and
A15: not <*k*> is_a_proper_prefix_of s ; ::_thesis: b1 in tree q
now__::_thesis:_s_in_tree_q
percases ( s = {} or ex n being Element of NAT ex r being FinSequence st
( n < len p & r in p . (n + 1) & s = <*n*> ^ r ) ) by A14, TREES_3:def_15;
suppose s = {} ; ::_thesis: s in tree q
hence  s in tree q by TREES_1:22; ::_thesis: verum
end;
suppose ex n being Element of NAT ex r being FinSequence st
( n < len p & r in p . (n + 1) & s = <*n*> ^ r ) ; ::_thesis: s in tree q
then consider n being Element of NAT , r being FinSequence such that
A16: n < len p and
A17: r in p . (n + 1) and
A18: s = <*n*> ^ r ;
now__::_thesis:_s_in_tree_q
percases ( r = {} or r <> {} ) ;
supposeA19: r = {} ; ::_thesis: s in tree q
 ( 1 <= n + 1 & n + 1 <= len q ) by A1, A16, NAT_1:11, NAT_1:13;
then  n + 1 in dom q by FINSEQ_3:25;
then  q . (n + 1) is Tree by TREES_3:22;
then  r in q . (n + 1) by A19, TREES_1:22;
hence  s in tree q by A1, A16, A18, TREES_3:def_15; ::_thesis: verum
end;
supposeA20: r <> {} ; ::_thesis: s in tree q
A21: now__::_thesis:_not_n_=_k
assume  n = k ; ::_thesis: contradiction
then  ( <*k*> is_a_prefix_of s & not s = <*k*> ) by A18, A20, FINSEQ_1:87, TREES_1:1;
hence  contradiction by A15, XBOOLE_0:def_8; ::_thesis: verum
end;
 ( 1 <= n + 1 & n + 1 <= len p ) by A16, NAT_1:11, NAT_1:13;
then  n + 1 in dom p by FINSEQ_3:25;
then  q . (n + 1) = p . (n + 1) by A3, A21, XCMPLX_1:2;
hence  s in tree q by A1, A16, A17, A18, TREES_3:def_15; ::_thesis: verum
end;
end;
end;
hence  s in tree q ; ::_thesis: verum
end;
end;
end;
hence  s in tree q ; ::_thesis: verum
end;
suppose ex r being FinSequence of NAT st
( r in t & s = <*k*> ^ r ) ; ::_thesis: b1 in tree q
hence  s in tree q by A1, A4, A5, TREES_3:def_15; ::_thesis: verum
end;
end;
end;
 p . (k + 1) is Tree by A2, TREES_3:22;
then A22: {} in p . (k + 1) by TREES_1:22;
 <*k*> = <*k*> ^ {} by FINSEQ_1:34;
then  <*k*> in tree p by A4, A22, TREES_3:def_15;
hence  tree q = (tree p) with-replacement (<*k*>,t) by A6, TREES_1:def_9; ::_thesis: verum
end;

theorem :: PRE_CIRC:15
for e1, e2 being finite DecoratedTree
for x being set
for k being Element of NAT
for p being DTree-yielding FinSequence st <*k*> in dom e1 & e1 = x -tree p holds
ex q being DTree-yielding FinSequence st
( e1 with-replacement (<*k*>,e2) = x -tree q & len q = len p & q . (k + 1) = e2 & ( for i being Element of NAT st i in dom p & i <> k + 1 holds
q . i = p . i ) )
proof
let e1, e2 be finite DecoratedTree; ::_thesis: for x being set
for k being Element of NAT
for p being DTree-yielding FinSequence st <*k*> in dom e1 & e1 = x -tree p holds
ex q being DTree-yielding FinSequence st
( e1 with-replacement (<*k*>,e2) = x -tree q & len q = len p & q . (k + 1) = e2 & ( for i being Element of NAT st i in dom p & i <> k + 1 holds
q . i = p . i ) )
let x be set ; ::_thesis: for k being Element of NAT
for p being DTree-yielding FinSequence st <*k*> in dom e1 & e1 = x -tree p holds
ex q being DTree-yielding FinSequence st
( e1 with-replacement (<*k*>,e2) = x -tree q & len q = len p & q . (k + 1) = e2 & ( for i being Element of NAT st i in dom p & i <> k + 1 holds
q . i = p . i ) )
let k be Element of NAT ; ::_thesis: for p being DTree-yielding FinSequence st <*k*> in dom e1 & e1 = x -tree p holds
ex q being DTree-yielding FinSequence st
( e1 with-replacement (<*k*>,e2) = x -tree q & len q = len p & q . (k + 1) = e2 & ( for i being Element of NAT st i in dom p & i <> k + 1 holds
q . i = p . i ) )
let p be DTree-yielding FinSequence; ::_thesis: ( <*k*> in dom e1 & e1 = x -tree p implies ex q being DTree-yielding FinSequence st
( e1 with-replacement (<*k*>,e2) = x -tree q & len q = len p & q . (k + 1) = e2 & ( for i being Element of NAT st i in dom p & i <> k + 1 holds
q . i = p . i ) ) )
assume that
A1: <*k*> in dom e1 and
A2: e1 = x -tree p ; ::_thesis: ex q being DTree-yielding FinSequence st
( e1 with-replacement (<*k*>,e2) = x -tree q & len q = len p & q . (k + 1) = e2 & ( for i being Element of NAT st i in dom p & i <> k + 1 holds
q . i = p . i ) )
consider j being Element of NAT , T being DecoratedTree, w being Node of T such that
A3: j < len p and
 T = p . (j + 1) and
A4: <*k*> = <*j*> ^ w by A1, A2, TREES_4:11;
consider pp being DTree-yielding FinSequence such that
A5: p = pp and
A6: dom (x -tree p) = tree (doms pp) by TREES_4:def_4;
A7: dom (doms pp) = dom p by A5, TREES_3:37;
deffunc H1( Nat) ->  set = IFEQ ($1,(k + 1),e2,(p . $1));
set o = <*k*>;
consider q being FinSequence such that
A8: len q = len p and
A9: for i being Nat st i in dom q holds
q . i = H1(i) from FINSEQ_1:sch_2();
A10: dom q = Seg (len p) by A8, FINSEQ_1:def_3;
A11: dom q = dom p by A8, FINSEQ_3:29;
now__::_thesis:_for_x_being_set_st_x_in_dom_q_holds_
q_._x_is_DecoratedTree
let x be set ; ::_thesis: ( x in dom q implies q . x is DecoratedTree )
assume A12: x in dom q ; ::_thesis: q . x is DecoratedTree
then reconsider i = x as Element of NAT ;
A13: ( i = k + 1 or i <> k + 1 ) ;
 q . i = IFEQ (i,(k + 1),e2,(p . i)) by A9, A12;
then  ( q . i = e2 or q . i = p . i ) by A13, FUNCOP_1:def_8;
hence  q . x is DecoratedTree by A11, A12, TREES_3:24; ::_thesis: verum
end;
then reconsider q = q as DTree-yielding FinSequence by TREES_3:24;
consider qq being DTree-yielding FinSequence such that
A14: q = qq and
A15: dom (x -tree q) = tree (doms qq) by TREES_4:def_4;
A16: len (doms pp) = len p by A5, TREES_3:38
.= len (doms qq) by A8, A14, TREES_3:38 ;
A17: dom p = Seg (len p) by FINSEQ_1:def_3;
A18: now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_(doms_pp)_&_i_<>_k_+_1_holds_
(doms_pp)_._i_=_(doms_qq)_._i
let i be Element of NAT ; ::_thesis: ( i in dom (doms pp) & i <> k + 1 implies (doms pp) . i = (doms qq) . i )
assume that
A19: i in dom (doms pp) and
A20: i <> k + 1 ; ::_thesis: (doms pp) . i = (doms qq) . i
A21: q . i = IFEQ (i,(k + 1),e2,(p . i)) by A9, A10, A17, A7, A19
.= p . i by A20, FUNCOP_1:def_8 ;
reconsider pii = p . i as DecoratedTree by A7, A19, TREES_3:24;
thus (doms pp) . i = dom pii by A5, A7, A19, FUNCT_6:22
.= (doms qq) . i by A11, A14, A7, A19, A21, FUNCT_6:22 ; ::_thesis: verum
end;
reconsider dqq = doms qq as Tree-yielding FinSequence ;
take  q ; ::_thesis: ( e1 with-replacement (<*k*>,e2) = x -tree q & len q = len p & q . (k + 1) = e2 & ( for i being Element of NAT st i in dom p & i <> k + 1 holds
q . i = p . i ) )
 <*j*> = <*k*> by A4, FINSEQ_1:88;
then A22: j = <*k*> . 1 by FINSEQ_1:def_8
.= k by FINSEQ_1:def_8 ;
then  ( 1 <= k + 1 & k + 1 <= len p ) by A3, NAT_1:11, NAT_1:13;
then A23: k + 1 in dom p by FINSEQ_3:25;
then  k + 1 in Seg (len p) by FINSEQ_1:def_3;
then A24: q . (k + 1) = IFEQ ((k + 1),(k + 1),e2,(p . (k + 1))) by A9, A10
.= e2 by FUNCOP_1:def_8 ;
then  (doms qq) . (k + 1) = dom e2 by A11, A23, A14, FUNCT_6:22;
then A25: dom (x -tree q) = (dom e1) with-replacement (<*k*>,(dom e2)) by A2, A23, A15, A6, A16, A7, A18, Th14;
 for f being FinSequence of NAT holds
( not f in (dom e1) with-replacement (<*k*>,(dom e2)) or ( not <*k*> is_a_prefix_of f & (x -tree q) . f = e1 . f ) or ex r being FinSequence of NAT st
( r in dom e2 & f = <*k*> ^ r & (x -tree q) . f = e2 . r ) )
proof
reconsider o9 = <*k*> as Element of dom e1 by A1;
let f be FinSequence of NAT ; ::_thesis: ( not f in (dom e1) with-replacement (<*k*>,(dom e2)) or ( not <*k*> is_a_prefix_of f & (x -tree q) . f = e1 . f ) or ex r being FinSequence of NAT st
( r in dom e2 & f = <*k*> ^ r & (x -tree q) . f = e2 . r ) )
assume A26: f in (dom e1) with-replacement (<*k*>,(dom e2)) ; ::_thesis: ( ( not <*k*> is_a_prefix_of f & (x -tree q) . f = e1 . f ) or ex r being FinSequence of NAT st
( r in dom e2 & f = <*k*> ^ r & (x -tree q) . f = e2 . r ) )
percases ( not o9 is_a_prefix_of f or ex t1 being Element of dom e2 st f = o9 ^ t1 ) by A26, Th11;
supposeA27: not o9 is_a_prefix_of f ; ::_thesis: ( ( not <*k*> is_a_prefix_of f & (x -tree q) . f = e1 . f ) or ex r being FinSequence of NAT st
( r in dom e2 & f = <*k*> ^ r & (x -tree q) . f = e2 . r ) )
A28: (x -tree q) . f = e1 . f
proof
percases ( f = {} or ex w being Element of NAT ex u being FinSequence st
( w < len dqq & u in dqq . (w + 1) & f = <*w*> ^ u ) ) by A15, A25, A26, TREES_3:def_15;
supposeA29: f = {} ; ::_thesis: (x -tree q) . f = e1 . f
hence (x -tree q) . f = x by TREES_4:def_4
.= e1 . f by A2, A29, TREES_4:def_4 ;
::_thesis: verum
end;
suppose ex w being Element of NAT ex u being FinSequence st
( w < len dqq & u in dqq . (w + 1) & f = <*w*> ^ u ) ; ::_thesis: (x -tree q) . f = e1 . f
then consider w being Element of NAT , u being FinSequence such that
A30: w < len (doms q) and
A31: u in (doms q) . (w + 1) and
A32: f = <*w*> ^ u by A14;
reconsider u = u as FinSequence of NAT by A32, FINSEQ_1:36;
reconsider ww = <*w*> as FinSequence of NAT ;
A33: w + 1 <> k + 1 by A27, A32, TREES_1:1;
A34: ex pp being DTree-yielding FinSequence st
( p = pp & dom (x -tree p) = tree (doms pp) ) by TREES_4:def_4;
A35: w < len q by A30, TREES_3:38;
then A36: (x -tree q) | <*w*> = q . (w + 1) by TREES_4:def_4;
 ( 1 <= w + 1 & w + 1 <= len p ) by A8, A35, NAT_1:11, NAT_1:13;
then A37: w + 1 in dom p by FINSEQ_3:25;
then reconsider pw1 = p . (w + 1) as DecoratedTree by TREES_3:24;
A38: q . (w + 1) = IFEQ ((w + 1),(k + 1),e2,(p . (w + 1))) by A9, A10, A17, A37
.= p . (w + 1) by A33, FUNCOP_1:def_8 ;
 w + 1 in dom (doms p) by A37, TREES_3:37;
then A39: (dom (x -tree p)) | <*w*> = (doms p) . (w + 1) by A34, Th12
.= dom pw1 by A37, FUNCT_6:22
.= (doms q) . (w + 1) by A11, A37, A38, FUNCT_6:22 ;
 w + 1 in dom (doms q) by A11, A37, TREES_3:37;
then  (dom (x -tree q)) | <*w*> = (doms q) . (w + 1) by A14, A15, Th12;
hence (x -tree q) . f = ((x -tree q) | ww) . u by A31, A32, TREES_2:def_10
.= ((x -tree p) | ww) . u by A8, A35, A36, A38, TREES_4:def_4
.= e1 . f by A2, A31, A32, A39, TREES_2:def_10 ;
::_thesis: verum
end;
end;
end;
assume  ( <*k*> is_a_prefix_of f or (x -tree q) . f <> e1 . f ) ; ::_thesis: ex r being FinSequence of NAT st
( r in dom e2 & f = <*k*> ^ r & (x -tree q) . f = e2 . r )
hence  ex r being FinSequence of NAT st
( r in dom e2 & f = <*k*> ^ r & (x -tree q) . f = e2 . r ) by A27, A28; ::_thesis: verum
end;
suppose ex t1 being Element of dom e2 st f = o9 ^ t1 ; ::_thesis: ( ( not <*k*> is_a_prefix_of f & (x -tree q) . f = e1 . f ) or ex r being FinSequence of NAT st
( r in dom e2 & f = <*k*> ^ r & (x -tree q) . f = e2 . r ) )
then consider r being Element of dom e2 such that
A40: f = <*k*> ^ r ;
assume  ( <*k*> is_a_prefix_of f or (x -tree q) . f <> e1 . f ) ; ::_thesis: ex r being FinSequence of NAT st
( r in dom e2 & f = <*k*> ^ r & (x -tree q) . f = e2 . r )
A41: (x -tree q) | <*k*> = q . (k + 1) by A8, A3, A22, TREES_4:def_4;
reconsider r = r as FinSequence of NAT ;
take  r ; ::_thesis: ( r in dom e2 & f = <*k*> ^ r & (x -tree q) . f = e2 . r )
thus A42: r in dom e2 ; ::_thesis: ( f = <*k*> ^ r & (x -tree q) . f = e2 . r )
thus  f = <*k*> ^ r by A40; ::_thesis: (x -tree q) . f = e2 . r
 r in (dom (x -tree q)) | <*k*> by A1, A25, A42, TREES_1:33;
hence  (x -tree q) . f = e2 . r by A24, A40, A41, TREES_2:def_10; ::_thesis: verum
end;
end;
end;
hence  e1 with-replacement (<*k*>,e2) = x -tree q by A1, A25, TREES_2:def_11; ::_thesis: ( len q = len p & q . (k + 1) = e2 & ( for i being Element of NAT st i in dom p & i <> k + 1 holds
q . i = p . i ) )
thus  len q = len p by A8; ::_thesis: ( q . (k + 1) = e2 & ( for i being Element of NAT st i in dom p & i <> k + 1 holds
q . i = p . i ) )
thus  q . (k + 1) = e2 by A24; ::_thesis: for i being Element of NAT st i in dom p & i <> k + 1 holds
q . i = p . i
let i be Element of NAT ; ::_thesis: ( i in dom p & i <> k + 1 implies q . i = p . i )
assume  i in dom p ; ::_thesis: ( not i <> k + 1 or q . i = p . i )
then  q . i = IFEQ (i,(k + 1),e2,(p . i)) by A9, A10, A17;
hence  ( not i <> k + 1 or q . i = p . i ) by FUNCOP_1:def_8; ::_thesis: verum
end;

theorem :: PRE_CIRC:16
for T being finite Tree
for p being Element of T st p <> {} holds
card (T | p) < card T
proof
let T be finite Tree; ::_thesis: for p being Element of T st p <> {} holds
card (T | p) < card T
let p be Element of T; ::_thesis: ( p <> {} implies card (T | p) < card T )
reconsider p9 = p as Element of NAT * by FINSEQ_1:def_11;
set X =  {  (p9 ^ n) where n is Element of NAT * : n in T | p  }  ;
A1: T | p, {  (p9 ^ n) where n is Element of NAT * : n in T | p  }  are_equipotent
proof
deffunc H1( Element of T | p) ->  FinSequence of NAT = p9 ^ $1;
consider f being Function such that
A2: dom f = T | p and
A3: for n being Element of T | p holds f . n = H1(n) from FUNCT_1:sch_4();
take  f ; :: according to WELLORD2:def_4 ::_thesis: ( f is one-to-one & proj1 f = T | p & proj2 f =  {  (p9 ^ n) where n is Element of NAT * : n in T | p  }  )
thus  f is one-to-one ::_thesis: ( proj1 f = T | p & proj2 f =  {  (p9 ^ n) where n is Element of NAT * : n in T | p  }  )
proof
let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds
( not x in proj1 f or not b1 in proj1 f or not f . x = f . b1 or x = b1 )
let y be set ; ::_thesis: ( not x in proj1 f or not y in proj1 f or not f . x = f . y or x = y )
assume that
A4: ( x in dom f & y in dom f ) and
A5: f . x = f . y ; ::_thesis: x = y
reconsider m = x, n = y as Element of T | p by A2, A4;
p9 ^ m = f . n by A3, A5
.= p9 ^ n by A3 ;
hence  x = y by FINSEQ_1:33; ::_thesis: verum
end;
thus  dom f = T | p by A2; ::_thesis: proj2 f =  {  (p9 ^ n) where n is Element of NAT * : n in T | p  }
thus  rng f c=  {  (p9 ^ n) where n is Element of NAT * : n in T | p  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  (p9 ^ n) where n is Element of NAT * : n in T | p  }  c= proj2 f
proof
let i be set ; :: according to TARSKI:def_3 ::_thesis: ( not i in rng f or i in  {  (p9 ^ n) where n is Element of NAT * : n in T | p  }  )
assume  i in rng f ; ::_thesis: i in  {  (p9 ^ n) where n is Element of NAT * : n in T | p  }
then consider n being set  such that
A6: n in dom f and
A7: i = f . n by FUNCT_1:def_3;
 T | p c= NAT * by TREES_1:def_3;
then reconsider n = n as Element of NAT * by A2, A6;
 f . n = p9 ^ n by A2, A3, A6;
hence  i in  {  (p9 ^ n) where n is Element of NAT * : n in T | p  }  by A2, A6, A7; ::_thesis: verum
end;
let i be set ; :: according to TARSKI:def_3 ::_thesis: ( not i in  {  (p9 ^ n) where n is Element of NAT * : n in T | p  }  or i in proj2 f )
assume  i in  {  (p9 ^ n) where n is Element of NAT * : n in T | p  }  ; ::_thesis: i in proj2 f
then consider n being Element of NAT *  such that
A8: i = p9 ^ n and
A9: n in T | p ;
reconsider n = n as Element of T | p by A9;
 i = f . n by A3, A8;
hence  i in proj2 f by A2, FUNCT_1:def_3; ::_thesis: verum
end;
then reconsider X =  {  (p9 ^ n) where n is Element of NAT * : n in T | p  }  as finite set by CARD_1:38;
A10: card X = card (T | p) by A1, CARD_1:5;
assume A11: p <> {} ; ::_thesis: card (T | p) < card T
A12: X <> T
proof
assume  X = T ; ::_thesis: contradiction
then  {} in X by TREES_1:22;
then  ex n being Element of NAT * st
( {} = p9 ^ n & n in T | p ) ;
hence  contradiction by A11; ::_thesis: verum
end;
 X c= T
proof
let i be set ; :: according to TARSKI:def_3 ::_thesis: ( not i in X or i in T )
assume  i in X ; ::_thesis: i in T
then  ex n being Element of NAT * st
( i = p9 ^ n & n in T | p ) ;
hence  i in T by TREES_1:def_6; ::_thesis: verum
end;
then  X c< T by A12, XBOOLE_0:def_8;
hence  card (T | p) < card T by A10, CARD_2:48; ::_thesis: verum
end;

theorem Th17: :: PRE_CIRC:17
for T, T1 being finite Tree
for p being Element of T holds (card (T with-replacement (p,T1))) + (card (T | p)) = (card T) + (card T1)
proof
let T, T1 be finite Tree; ::_thesis: for p being Element of T holds (card (T with-replacement (p,T1))) + (card (T | p)) = (card T) + (card T1)
let p be Element of T; ::_thesis: (card (T with-replacement (p,T1))) + (card (T | p)) = (card T) + (card T1)
defpred S1[ Element of T] means  not p is_a_prefix_of $1;
defpred S2[ Element of T] means p is_a_prefix_of $1;
set A =  {  t where t is Element of T : S1[t]  }  ;
set B =  {  t where t is Element of T : S2[t]  }  ;
set C =  {  (p ^ t1) where t1 is Element of T1 : verum  }  ;
A1:  {  t where t is Element of T : S1[t]  }  is Subset of T from DOMAIN_1:sch_7();
A2:  {  t where t is Element of T : S2[t]  }  is Subset of T from DOMAIN_1:sch_7();
A3: T1, {  (p ^ t1) where t1 is Element of T1 : verum  }  are_equipotent
proof
deffunc H1( Element of T1) ->  FinSequence of NAT = p ^ $1;
consider f being Function such that
A4: dom f = T1 and
A5: for n being Element of T1 holds f . n = H1(n) from FUNCT_1:sch_4();
take  f ; :: according to WELLORD2:def_4 ::_thesis: ( f is one-to-one & proj1 f = T1 & proj2 f =  {  (p ^ t1) where t1 is Element of T1 : verum  }  )
thus  f is one-to-one ::_thesis: ( proj1 f = T1 & proj2 f =  {  (p ^ t1) where t1 is Element of T1 : verum  }  )
proof
let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds
( not x in proj1 f or not b1 in proj1 f or not f . x = f . b1 or x = b1 )
let y be set ; ::_thesis: ( not x in proj1 f or not y in proj1 f or not f . x = f . y or x = y )
assume that
A6: ( x in dom f & y in dom f ) and
A7: f . x = f . y ; ::_thesis: x = y
reconsider m = x, n = y as Element of T1 by A4, A6;
p ^ m = f . n by A5, A7
.= p ^ n by A5 ;
hence  x = y by FINSEQ_1:33; ::_thesis: verum
end;
thus  dom f = T1 by A4; ::_thesis: proj2 f =  {  (p ^ t1) where t1 is Element of T1 : verum  }
thus  rng f c=  {  (p ^ t1) where t1 is Element of T1 : verum  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  (p ^ t1) where t1 is Element of T1 : verum  }  c= proj2 f
proof
let i be set ; :: according to TARSKI:def_3 ::_thesis: ( not i in rng f or i in  {  (p ^ t1) where t1 is Element of T1 : verum  }  )
assume  i in rng f ; ::_thesis: i in  {  (p ^ t1) where t1 is Element of T1 : verum  }
then consider n being set  such that
A8: n in dom f and
A9: i = f . n by FUNCT_1:def_3;
 T1 c= NAT * by TREES_1:def_3;
then reconsider n = n as Element of NAT * by A4, A8;
 f . n = p ^ n by A4, A5, A8;
hence  i in  {  (p ^ t1) where t1 is Element of T1 : verum  }  by A4, A8, A9; ::_thesis: verum
end;
let i be set ; :: according to TARSKI:def_3 ::_thesis: ( not i in  {  (p ^ t1) where t1 is Element of T1 : verum  }  or i in proj2 f )
assume  i in  {  (p ^ t1) where t1 is Element of T1 : verum  }  ; ::_thesis: i in proj2 f
then consider n being Element of T1 such that
A10: i = p ^ n ;
 i = f . n by A5, A10;
hence  i in proj2 f by A4, FUNCT_1:def_3; ::_thesis: verum
end;
reconsider A =  {  t where t is Element of T : S1[t]  }  , B =  {  t where t is Element of T : S2[t]  }  as finite set by A1, A2;
now__::_thesis:_for_x_being_set_holds_
(_(_not_x_in_T_or_x_in_A_or_x_in_B_)_&_(_(_x_in_A_or_x_in_B_)_implies_x_in_T_)_)
let x be set ; ::_thesis: ( ( not x in T or x in A or x in B ) & ( ( x in A or x in B ) implies x in T ) )
hereby  ::_thesis: ( ( x in A or x in B ) implies x in T )
assume  x in T ; ::_thesis: ( x in A or x in B )
then reconsider t = x as Element of T ;
 ( p is_a_prefix_of t or not p is_a_prefix_of t ) ;
hence  ( x in A or x in B ) ; ::_thesis: verum
end;
assume  ( x in A or x in B ) ; ::_thesis: x in T
hence  x in T by A1, A2; ::_thesis: verum
end;
then A11: T = A \/ B by XBOOLE_0:def_3;
A12: A misses  {  (p ^ t1) where t1 is Element of T1 : verum  }
proof
assume  not A misses  {  (p ^ t1) where t1 is Element of T1 : verum  }  ; ::_thesis: contradiction
then consider x being set  such that
A13: x in A /\  {  (p ^ t1) where t1 is Element of T1 : verum  }  by XBOOLE_0:4;
 x in  {  (p ^ t1) where t1 is Element of T1 : verum  }  by A13, XBOOLE_0:def_4;
then A14: ex t1 being Element of T1 st x = p ^ t1 ;
 x in A by A13, XBOOLE_0:def_4;
then  ex t being Element of T st
( x = t & not p is_a_prefix_of t ) ;
hence  contradiction by A14, TREES_1:1; ::_thesis: verum
end;
A15: A misses B
proof
assume  not A misses B ; ::_thesis: contradiction
then consider x being set  such that
A16: x in A /\ B by XBOOLE_0:4;
 x in B by A16, XBOOLE_0:def_4;
then A17: ex t being Element of T st
( x = t & p is_a_prefix_of t ) ;
 x in A by A16, XBOOLE_0:def_4;
then  ex t being Element of T st
( x = t & not p is_a_prefix_of t ) ;
hence  contradiction by A17; ::_thesis: verum
end;
A18: T with-replacement (p,T1) = A \/  {  (p ^ t1) where t1 is Element of T1 : verum  }  by Th10;
reconsider C =  {  (p ^ t1) where t1 is Element of T1 : verum  }  as finite set by A3, CARD_1:38;
A19: card T1 = card C by A3, CARD_1:5;
 T | p,B are_equipotent by Th9;
then  card (T | p) = card B by CARD_1:5;
hence (card (T with-replacement (p,T1))) + (card (T | p)) = ((card A) + (card C)) + (card B) by A18, A12, CARD_2:40
.= ((card A) + (card B)) + (card C)
.= (card T) + (card T1) by A11, A15, A19, CARD_2:40 ;
::_thesis: verum
end;

theorem :: PRE_CIRC:18
for T, T1 being finite DecoratedTree
for p being Element of dom T holds (card (T with-replacement (p,T1))) + (card (T | p)) = (card T) + (card T1)
proof
let T, T1 be finite DecoratedTree; ::_thesis: for p being Element of dom T holds (card (T with-replacement (p,T1))) + (card (T | p)) = (card T) + (card T1)
let p be Element of dom T; ::_thesis: (card (T with-replacement (p,T1))) + (card (T | p)) = (card T) + (card T1)
A1: ( card (dom T) = card T & card (dom T1) = card T1 ) by CARD_1:62;
A2: ( card (dom (T with-replacement (p,T1))) = card (T with-replacement (p,T1)) & card (dom (T | p)) = card (T | p) ) by CARD_1:62;
 ( dom (T with-replacement (p,T1)) = (dom T) with-replacement (p,(dom T1)) & dom (T | p) = (dom T) | p ) by TREES_2:def_10, TREES_2:def_11;
hence  (card (T with-replacement (p,T1))) + (card (T | p)) = (card T) + (card T1) by A1, A2, Th17; ::_thesis: verum
end;

registration
let x be set ;
cluster root-tree x ->  finite ;
coherence
 root-tree x is finite
proof
 root-tree x = {[{},x]} by TREES_4:6;
hence  root-tree x is finite ; ::_thesis: verum
end;
end;

theorem :: PRE_CIRC:19
for x being set holds card (root-tree x) = 1
proof
let x be set ; ::_thesis: card (root-tree x) = 1
 root-tree x = {[{},x]} by TREES_4:6;
hence  card (root-tree x) = 1 by CARD_1:30; ::_thesis: verum
end;

begin

theorem :: PRE_CIRC:20
for F being non empty finite set holds (card F) - 1 = (card F) -' 1
proof
let F be non empty finite set ; ::_thesis: (card F) - 1 = (card F) -' 1
 (card F) - 1 >= 0 by NAT_1:14, XREAL_1:48;
hence  (card F) - 1 = (card F) -' 1 by XREAL_0:def_2; ::_thesis: verum
end;

theorem :: PRE_CIRC:21
for f, g being Function holds
( dom f, dom g are_equipotent iff f,g are_equipotent )
proof
let f, g be Function; ::_thesis: ( dom f, dom g are_equipotent iff f,g are_equipotent )
A1: ( card f = card (dom f) & card g = card (dom g) ) by CARD_1:62;
hereby  ::_thesis: ( f,g are_equipotent implies dom f, dom g are_equipotent )
assume  dom f, dom g are_equipotent ; ::_thesis: f,g are_equipotent
then  card (dom f) = card (dom g) by CARD_1:5;
hence  f,g are_equipotent by A1, CARD_1:5; ::_thesis: verum
end;
assume  f,g are_equipotent ; ::_thesis: dom f, dom g are_equipotent
then  card f = card g by CARD_1:5;
hence  dom f, dom g are_equipotent by A1, CARD_1:5; ::_thesis: verum
end;

theorem :: PRE_CIRC:22
for f, g being finite Function st dom f misses dom g holds
card (f +* g) = (card f) + (card g)
proof
let f, g be finite Function; ::_thesis: ( dom f misses dom g implies card (f +* g) = (card f) + (card g) )
assume A1: dom f misses dom g ; ::_thesis: card (f +* g) = (card f) + (card g)
thus  card (f +* g) = card (dom (f +* g)) by CARD_1:62
.= card ((dom f) \/ (dom g)) by FUNCT_4:def_1
.= (card (dom f)) + (card (dom g)) by A1, CARD_2:40
.= (card (dom f)) + (card g) by CARD_1:62
.= (card f) + (card g) by CARD_1:62 ; ::_thesis: verum
end;

theorem :: PRE_CIRC:23
for n being Nat holds  {  k where k is Element of NAT : k > n  }  is infinite
proof
let n be Nat; ::_thesis:  {  k where k is Element of NAT : k > n  }  is infinite
set X =  {  k where k is Element of NAT : k > n  }  ;
A1:  {  k where k is Element of NAT : k > n  }  c= NAT
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  k where k is Element of NAT : k > n  }  or x in NAT )
assume  x in  {  k where k is Element of NAT : k > n  }  ; ::_thesis: x in NAT
then  ex k being Element of NAT st
( x = k & k > n ) ;
hence  x in NAT ; ::_thesis: verum
end;
 n + 1 > n + 0 by XREAL_1:8;
then A2: n + 1 in  {  k where k is Element of NAT : k > n  }  ;
assume   {  k where k is Element of NAT : k > n  }  is finite ; ::_thesis: contradiction
then reconsider X =  {  k where k is Element of NAT : k > n  }  as non empty finite Subset of NAT by A1, A2;
set m = max X;
 max X in X by XXREAL_2:def_8;
then consider k being Element of NAT  such that
A3: max X = k and
A4: k > n ;
 k + 1 > k + 0 by XREAL_1:8;
then  k + 1 > n by A4, XXREAL_0:2;
then  (max X) + 1 in X by A3;
then  (max X) + 1 <= (max X) + 0 by XXREAL_2:def_8;
hence  contradiction by XREAL_1:8; ::_thesis: verum
end;