let k be Nat; :: thesis: for s, t being finite binary DecoratedTree of IndexedREAL holds union (LeavesSet {s,t}) = union (LeavesSet {(MakeTree (t,s,k))})
let s, t be finite binary DecoratedTree of IndexedREAL ; :: thesis: union (LeavesSet {s,t}) = union (LeavesSet {(MakeTree (t,s,k))})
A1: {s} \/ {t} = union {{s},{t}} by ZFMISC_1:75
.= {s,t} by ZFMISC_1:26 ;
thus union (LeavesSet {s,t}) = union ((LeavesSet {s}) \/ (LeavesSet {t})) by Th8, A1
.= (union (LeavesSet {s})) \/ (union (LeavesSet {t})) by ZFMISC_1:78
.= (union {(Leaves s)}) \/ (union (LeavesSet {t})) by Th7
.= (union {(Leaves s)}) \/ (union {(Leaves t)}) by Th7
.= (Leaves s) \/ (union {(Leaves t)}) by ZFMISC_1:25
.= (Leaves s) \/ (Leaves t) by ZFMISC_1:25
.= Leaves (MakeTree (t,s,k)) by Th13
.= union {(Leaves (MakeTree (t,s,k)))} by ZFMISC_1:25
.= union (LeavesSet {(MakeTree (t,s,k))}) by Th7 ; :: thesis: verum