let D1, D2 be non empty set ; :: thesis: for d1 being Element of D1
for d2 being Element of D2 holds
( (root-tree [d1,d2]) `1 = root-tree d1 & (root-tree [d1,d2]) `2 = root-tree d2 )
let d1 be Element of D1; :: thesis: for d2 being Element of D2 holds
( (root-tree [d1,d2]) `1 = root-tree d1 & (root-tree [d1,d2]) `2 = root-tree d2 )
let d2 be Element of D2; :: thesis: ( (root-tree [d1,d2]) `1 = root-tree d1 & (root-tree [d1,d2]) `2 = root-tree d2 )
reconsider r = {} as Node of (root-tree [d1,d2]) by TREES_1:47;
A1: dom ((root-tree [d1,d2]) `1 ) = dom (root-tree [d1,d2]) by Th24;
A2: dom ((root-tree [d1,d2]) `2 ) = dom (root-tree [d1,d2]) by Th24;
A3: (root-tree [d1,d2]) . r = [d1,d2] by Th3;
A4: [d1,d2] `1 = d1 by MCART_1:7;
A5: [d1,d2] `2 = d2 by MCART_1:7;
thus (root-tree [d1,d2]) `1 = root-tree (((root-tree [d1,d2]) `1 ) . r) by A1, Th3, Th5
.= root-tree d1 by A3, A4, TREES_3:41 ; :: thesis: (root-tree [d1,d2]) `2 = root-tree d2
thus (root-tree [d1,d2]) `2 = root-tree (((root-tree [d1,d2]) `2 ) . r) by A2, Th3, Th5
.= root-tree d2 by A3, A5, TREES_3:41 ; :: thesis: verum