let s, t be DecoratedTree; for x being object holds Leaves (x -tree (t,s)) = (Leaves t) \/ (Leaves s)
let x be object ; Leaves (x -tree (t,s)) = (Leaves t) \/ (Leaves s)
set q = <*(dom t),(dom s)*>;
A1:
len <*(dom t),(dom s)*> = 2
by FINSEQ_1:44;
A2:
<*(dom t),(dom s)*> . 1 = dom t
by FINSEQ_1:44;
A3:
<*(dom t),(dom s)*> . 2 = dom s
by FINSEQ_1:44;
A4:
dom (x -tree (t,s)) = tree ((dom t),(dom s))
by TREES_4:14;
A5:
Leaves (tree ((dom t),(dom s))) = { (<*0*> ^ p) where p is Element of dom t : p in Leaves (dom t) } \/ { (<*1*> ^ p) where p is Element of dom s : p in Leaves (dom s) }
by Th10;
set L = { (<*0*> ^ p) where p is Element of dom t : p in Leaves (dom t) } ;
set R = { (<*1*> ^ p) where p is Element of dom s : p in Leaves (dom s) } ;
A6:
Leaves (x -tree (t,s)) = ((x -tree (t,s)) .: { (<*0*> ^ p) where p is Element of dom t : p in Leaves (dom t) } ) \/ ((x -tree (t,s)) .: { (<*1*> ^ p) where p is Element of dom s : p in Leaves (dom s) } )
by RELAT_1:120, A5, A4;
for z being object holds
( z in (x -tree (t,s)) .: { (<*0*> ^ p) where p is Element of dom t : p in Leaves (dom t) } iff z in t .: (Leaves (dom t)) )
proof
let z be
object ;
( z in (x -tree (t,s)) .: { (<*0*> ^ p) where p is Element of dom t : p in Leaves (dom t) } iff z in t .: (Leaves (dom t)) )
assume
z in t .: (Leaves (dom t))
;
z in (x -tree (t,s)) .: { (<*0*> ^ p) where p is Element of dom t : p in Leaves (dom t) }
then consider p0 being
object such that A9:
(
p0 in dom t &
p0 in Leaves (dom t) &
z = t . p0 )
by FUNCT_1:def 6;
reconsider p =
p0 as
Element of
dom t by A9;
A10:
(x -tree (t,s)) . (<*0*> ^ p) = t . p
by Th11;
(
0 < len <*(dom t),(dom s)*> &
p in <*(dom t),(dom s)*> . (0 + 1) )
by A2;
then A11:
<*0*> ^ p in dom (x -tree (t,s))
by TREES_3:def 15, A4;
<*0*> ^ p in { (<*0*> ^ p) where p is Element of dom t : p in Leaves (dom t) }
by A9;
hence
z in (x -tree (t,s)) .: { (<*0*> ^ p) where p is Element of dom t : p in Leaves (dom t) }
by A10, A9, FUNCT_1:def 6, A11;
verum
end;
then A12:
(x -tree (t,s)) .: { (<*0*> ^ p) where p is Element of dom t : p in Leaves (dom t) } = t .: (Leaves (dom t))
by TARSKI:2;
for z being object holds
( z in (x -tree (t,s)) .: { (<*1*> ^ p) where p is Element of dom s : p in Leaves (dom s) } iff z in s .: (Leaves (dom s)) )
proof
let z be
object ;
( z in (x -tree (t,s)) .: { (<*1*> ^ p) where p is Element of dom s : p in Leaves (dom s) } iff z in s .: (Leaves (dom s)) )
assume
z in s .: (Leaves (dom s))
;
z in (x -tree (t,s)) .: { (<*1*> ^ p) where p is Element of dom s : p in Leaves (dom s) }
then consider p0 being
object such that A15:
(
p0 in dom s &
p0 in Leaves (dom s) &
z = s . p0 )
by FUNCT_1:def 6;
reconsider p =
p0 as
Element of
dom s by A15;
A16:
(x -tree (t,s)) . (<*1*> ^ p) = s . p
by Th12;
( 1
< len <*(dom t),(dom s)*> &
p in <*(dom t),(dom s)*> . (1 + 1) )
by A1, A3;
then A17:
<*1*> ^ p in dom (x -tree (t,s))
by TREES_3:def 15, A4;
<*1*> ^ p in { (<*1*> ^ p) where p is Element of dom s : p in Leaves (dom s) }
by A15;
hence
z in (x -tree (t,s)) .: { (<*1*> ^ p) where p is Element of dom s : p in Leaves (dom s) }
by A16, A15, FUNCT_1:def 6, A17;
verum
end;
hence
Leaves (x -tree (t,s)) = (Leaves t) \/ (Leaves s)
by A6, A12, TARSKI:2; verum