let s, t be DecoratedTree; :: thesis: for x being object holds Leaves (x -tree (t,s)) = (Leaves t) \/ (Leaves s)
let x be object ; :: thesis: 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;
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 ; :: thesis: ( 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)) )

hereby :: thesis: ( z in t .: (Leaves (dom t)) implies z in (x -tree (t,s)) .: { (<*0*> ^ p) where p is Element of dom t : p in Leaves (dom t) } )

assume z in (x -tree (t,s)) .: { (<*0*> ^ p) where p is Element of dom t : p in Leaves (dom t) } ; :: thesis: z in t .: (Leaves (dom t))
then consider q being object such that
A7: ( q in dom (x -tree (t,s)) & q in { (<*0*> ^ p) where p is Element of dom t : p in Leaves (dom t) } & z = (x -tree (t,s)) . q ) by FUNCT_1:def 6;
consider p being Element of dom t such that
A8: ( q = <*0*> ^ p & p in Leaves (dom t) ) by A7;
z = t . p by A7, Th11, A8;
hence z in t .: (Leaves (dom t)) by A8, FUNCT_1:def 6; :: thesis: verum

end;

assume z in t .: (Leaves (dom t)) ; :: thesis: 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) ) ;
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; :: thesis: 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 ; :: thesis: ( 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)) )

hereby :: thesis: ( z in s .: (Leaves (dom s)) implies z in (x -tree (t,s)) .: { (<*1*> ^ p) where p is Element of dom s : p in Leaves (dom s) } )

assume z in (x -tree (t,s)) .: { (<*1*> ^ p) where p is Element of dom s : p in Leaves (dom s) } ; :: thesis: z in s .: (Leaves (dom s))
then consider q being object such that
A13: ( q in dom (x -tree (t,s)) & q in { (<*1*> ^ p) where p is Element of dom s : p in Leaves (dom s) } & z = (x -tree (t,s)) . q ) by FUNCT_1:def 6;
consider p being Element of dom s such that
A14: ( q = <*1*> ^ p & p in Leaves (dom s) ) by A13;
(x -tree (t,s)) . (<*1*> ^ p) = s . p by Th12;
hence z in s .: (Leaves (dom s)) by A14, FUNCT_1:def 6, A13; :: thesis: verum

end;

assume z in s .: (Leaves (dom s)) ; :: thesis: 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;
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; :: thesis: verum

end;

hence Leaves (x -tree (t,s)) = (Leaves t) \/ (Leaves s) by A6, A12, TARSKI:2; :: thesis: verum