let X be non empty finite Subset of (BinFinTrees IndexedREAL); for s, t being finite binary DecoratedTree of IndexedREAL st s is one-to-one & t is one-to-one & t in X & s in X & (rng s) /\ (rng t) = {} & ( for z being finite binary DecoratedTree of IndexedREAL st z in X holds
not [((MaxVl X) + 1),((Vrootr t) + (Vrootr s))] in rng z ) holds
MakeTree (t,s,((MaxVl X) + 1)) is one-to-one
let s, t be finite binary DecoratedTree of IndexedREAL ; ( s is one-to-one & t is one-to-one & t in X & s in X & (rng s) /\ (rng t) = {} & ( for z being finite binary DecoratedTree of IndexedREAL st z in X holds
not [((MaxVl X) + 1),((Vrootr t) + (Vrootr s))] in rng z ) implies MakeTree (t,s,((MaxVl X) + 1)) is one-to-one )
assume A1:
( s is one-to-one & t is one-to-one & t in X & s in X & (rng s) /\ (rng t) = {} & ( for z being finite binary DecoratedTree of IndexedREAL st z in X holds
not [((MaxVl X) + 1),((Vrootr t) + (Vrootr s))] in rng z ) )
; MakeTree (t,s,((MaxVl X) + 1)) is one-to-one
set d = MakeTree (t,s,((MaxVl X) + 1));
A2:
(MakeTree (t,s,((MaxVl X) + 1))) . {} = [((MaxVl X) + 1),((Vrootr t) + (Vrootr s))]
by TREES_4:def 4;
set bx = [((MaxVl X) + 1),((Vrootr t) + (Vrootr s))];
set q = <*(dom t),(dom s)*>;
A3:
len <*(dom t),(dom s)*> = 2
by FINSEQ_1:44;
A4:
<*(dom t),(dom s)*> . 1 = dom t
by FINSEQ_1:44;
A5:
<*(dom t),(dom s)*> . 2 = dom s
by FINSEQ_1:44;
A6:
dom ([((MaxVl X) + 1),((Vrootr t) + (Vrootr s))] -tree (t,s)) = tree ((dom t),(dom s))
by TREES_4:14;
A7:
for a being object holds
( not a in dom (MakeTree (t,s,((MaxVl X) + 1))) or a = {} or ex f being Element of dom t st a = <*0*> ^ f or ex f being Element of dom s st a = <*1*> ^ f )
A10:
for x being object st x in dom (MakeTree (t,s,((MaxVl X) + 1))) & x <> {} holds
(MakeTree (t,s,((MaxVl X) + 1))) . x <> (MakeTree (t,s,((MaxVl X) + 1))) . {}
proof
let x be
object ;
( x in dom (MakeTree (t,s,((MaxVl X) + 1))) & x <> {} implies (MakeTree (t,s,((MaxVl X) + 1))) . x <> (MakeTree (t,s,((MaxVl X) + 1))) . {} )
assume A11:
(
x in dom (MakeTree (t,s,((MaxVl X) + 1))) &
x <> {} )
;
(MakeTree (t,s,((MaxVl X) + 1))) . x <> (MakeTree (t,s,((MaxVl X) + 1))) . {}
end;
A14:
for x1, x2 being object st x1 in dom (MakeTree (t,s,((MaxVl X) + 1))) & x2 in dom (MakeTree (t,s,((MaxVl X) + 1))) & (MakeTree (t,s,((MaxVl X) + 1))) . x1 = (MakeTree (t,s,((MaxVl X) + 1))) . x2 & ex f being Element of dom s st x1 = <*1*> ^ f holds
for f being Element of dom t holds not x2 = <*0*> ^ f
proof
let x1,
x2 be
object ;
( x1 in dom (MakeTree (t,s,((MaxVl X) + 1))) & x2 in dom (MakeTree (t,s,((MaxVl X) + 1))) & (MakeTree (t,s,((MaxVl X) + 1))) . x1 = (MakeTree (t,s,((MaxVl X) + 1))) . x2 & ex f being Element of dom s st x1 = <*1*> ^ f implies for f being Element of dom t holds not x2 = <*0*> ^ f )
assume A15:
(
x1 in dom (MakeTree (t,s,((MaxVl X) + 1))) &
x2 in dom (MakeTree (t,s,((MaxVl X) + 1))) &
(MakeTree (t,s,((MaxVl X) + 1))) . x1 = (MakeTree (t,s,((MaxVl X) + 1))) . x2 )
;
( for f being Element of dom s holds not x1 = <*1*> ^ f or for f being Element of dom t holds not x2 = <*0*> ^ f )
assume A16:
( ex
f being
Element of
dom s st
x1 = <*1*> ^ f & ex
f being
Element of
dom t st
x2 = <*0*> ^ f )
;
contradiction
then consider f being
Element of
dom s such that A17:
x1 = <*1*> ^ f
;
A18:
(MakeTree (t,s,((MaxVl X) + 1))) . x1 = s . f
by A17, Th12;
consider g being
Element of
dom t such that A19:
x2 = <*0*> ^ g
by A16;
A20:
s . f = t . g
by A15, A18, A19, Th11;
(
s . f in rng s &
t . g in rng t )
by FUNCT_1:3;
hence
contradiction
by A1, XBOOLE_0:def 4, A20;
verum
end;
for x1, x2 being object st x1 in dom (MakeTree (t,s,((MaxVl X) + 1))) & x2 in dom (MakeTree (t,s,((MaxVl X) + 1))) & (MakeTree (t,s,((MaxVl X) + 1))) . x1 = (MakeTree (t,s,((MaxVl X) + 1))) . x2 holds
x1 = x2
proof
let x1,
x2 be
object ;
( x1 in dom (MakeTree (t,s,((MaxVl X) + 1))) & x2 in dom (MakeTree (t,s,((MaxVl X) + 1))) & (MakeTree (t,s,((MaxVl X) + 1))) . x1 = (MakeTree (t,s,((MaxVl X) + 1))) . x2 implies x1 = x2 )
assume A21:
(
x1 in dom (MakeTree (t,s,((MaxVl X) + 1))) &
x2 in dom (MakeTree (t,s,((MaxVl X) + 1))) &
(MakeTree (t,s,((MaxVl X) + 1))) . x1 = (MakeTree (t,s,((MaxVl X) + 1))) . x2 )
;
x1 = x2
per cases
( ( x1 = {} & x2 = {} ) or ( x1 = {} & x2 <> {} ) or ( x1 <> {} & x2 = {} ) or ( x1 <> {} & x2 <> {} ) )
;
suppose A22:
(
x1 <> {} &
x2 <> {} )
;
x1 = x2then A23:
( ex
f being
Element of
dom t st
x1 = <*0*> ^ f or ex
f being
Element of
dom s st
x1 = <*1*> ^ f )
by A21, A7;
A24:
( ex
f being
Element of
dom t st
x2 = <*0*> ^ f or ex
f being
Element of
dom s st
x2 = <*1*> ^ f )
by A21, A7, A22;
per cases
( ( ex f being Element of dom t st x1 = <*0*> ^ f & ex f being Element of dom t st x2 = <*0*> ^ f ) or ( ex f being Element of dom s st x1 = <*1*> ^ f & ex f being Element of dom s st x2 = <*1*> ^ f ) )
by A23, A24, A21, A14;
suppose A25:
( ex
f being
Element of
dom t st
x1 = <*0*> ^ f & ex
f being
Element of
dom t st
x2 = <*0*> ^ f )
;
x1 = x2then consider f being
Element of
dom t such that A26:
x1 = <*0*> ^ f
;
A27:
(MakeTree (t,s,((MaxVl X) + 1))) . x1 = t . f
by A26, Th11;
consider g being
Element of
dom t such that A28:
x2 = <*0*> ^ g
by A25;
(MakeTree (t,s,((MaxVl X) + 1))) . x2 = t . g
by A28, Th11;
hence
x1 = x2
by A26, A28, A1, FUNCT_1:def 4, A21, A27;
verum end; suppose A29:
( ex
f being
Element of
dom s st
x1 = <*1*> ^ f & ex
f being
Element of
dom s st
x2 = <*1*> ^ f )
;
x1 = x2then consider f being
Element of
dom s such that A30:
x1 = <*1*> ^ f
;
A31:
(MakeTree (t,s,((MaxVl X) + 1))) . x1 = s . f
by A30, Th12;
consider g being
Element of
dom s such that A32:
x2 = <*1*> ^ g
by A29;
(MakeTree (t,s,((MaxVl X) + 1))) . x2 = s . g
by A32, Th12;
hence
x1 = x2
by A30, A32, A1, FUNCT_1:def 4, A21, A31;
verum end; end; end; end;
end;
hence
MakeTree (t,s,((MaxVl X) + 1)) is one-to-one
by FUNCT_1:def 4; verum