let X be non empty finite Subset of (BinFinTrees IndexedREAL); :: thesis: 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 ; :: thesis: ( 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 ) ) ; :: thesis: 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;
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 )

proof

let a be object ; :: thesis: ( 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 )
assume A8: a in dom (MakeTree (t,s,((MaxVl X) + 1))) ; :: thesis: ( 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 )

per cases ( a = {} or ex n being Nat ex f being FinSequence st
( n < len <*(dom t),(dom s)*> & f in <*(dom t),(dom s)*> . (n + 1) & a = <*n*> ^ f ) ) by A6, TREES_3:def 15, A8;

suppose a = {} ; :: thesis: ( 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 )

hence ( 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 ) ; :: thesis: verum

end;

suppose ex n being Nat ex f being FinSequence st
( n < len <*(dom t),(dom s)*> & f in <*(dom t),(dom s)*> . (n + 1) & a = <*n*> ^ f ) ; :: thesis: ( 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 )

then consider n being Nat, f being FinSequence such that
A9: ( n < len <*(dom t),(dom s)*> & f in <*(dom t),(dom s)*> . (n + 1) & a = <*n*> ^ f ) ;

per cases ( n = 0 or n = 1 ) by NAT_1:23, A3, A9;

suppose n = 0 ; :: thesis: ( 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 )

hence ( 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 ) by A9; :: thesis: verum

end;

suppose n = 1 ; :: thesis: ( 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 )

hence ( 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 ) by A9; :: thesis: verum

end;

end;

end;

end;

end;

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 ; :: thesis: ( 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 <> {} ) ; :: thesis: (MakeTree (t,s,((MaxVl X) + 1))) . x <> (MakeTree (t,s,((MaxVl X) + 1))) . {}

per cases ( ex f being Element of dom t st x = <*0*> ^ f or ex f being Element of dom s st x = <*1*> ^ f ) by A11, A7;

suppose ex f being Element of dom t st x = <*0*> ^ f ; :: thesis: (MakeTree (t,s,((MaxVl X) + 1))) . x <> (MakeTree (t,s,((MaxVl X) + 1))) . {}

then consider f being Element of dom t such that
A12: x = <*0*> ^ f ;
(MakeTree (t,s,((MaxVl X) + 1))) . x = t . f by A12, Th11;
hence (MakeTree (t,s,((MaxVl X) + 1))) . x <> (MakeTree (t,s,((MaxVl X) + 1))) . {} by FUNCT_1:3, A1, A2; :: thesis: verum

end;

suppose ex f being Element of dom s st x = <*1*> ^ f ; :: thesis: (MakeTree (t,s,((MaxVl X) + 1))) . x <> (MakeTree (t,s,((MaxVl X) + 1))) . {}

then consider f being Element of dom s such that
A13: x = <*1*> ^ f ;
(MakeTree (t,s,((MaxVl X) + 1))) . x = s . f by A13, Th12;
hence (MakeTree (t,s,((MaxVl X) + 1))) . x <> (MakeTree (t,s,((MaxVl X) + 1))) . {} by FUNCT_1:3, A1, A2; :: thesis: verum

end;

end;

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 ; :: thesis: ( 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 ) ; :: thesis: ( 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 ) ; :: thesis: 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; :: thesis: 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 ; :: thesis: ( 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 ) ; :: thesis: x1 = x2

per cases ( ( x1 = {} & x2 = {} ) or ( x1 = {} & x2 <> {} ) or ( x1 <> {} & x2 = {} ) or ( x1 <> {} & x2 <> {} ) ) ;

suppose ( x1 = {} & x2 = {} ) ; :: thesis: x1 = x2

hence x1 = x2 ; :: thesis: verum

end;

suppose ( x1 = {} & x2 <> {} ) ; :: thesis: x1 = x2

hence x1 = x2 by A21, A10; :: thesis: verum

end;

suppose ( x1 <> {} & x2 = {} ) ; :: thesis: x1 = x2

hence x1 = x2 by A21, A10; :: thesis: verum

end;

suppose A22: ( x1 <> {} & x2 <> {} ) ; :: thesis: x1 = x2

then 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 ) ; :: thesis: x1 = x2

then 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; :: thesis: 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 ) ; :: thesis: x1 = x2

then 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; :: thesis: verum

end;

end;

end;

end;

end;

hence MakeTree (t,s,((MaxVl X) + 1)) is one-to-one by FUNCT_1:def 4; :: thesis: verum