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:22;
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] ;
A4: [d1,d2] `1 = d1 ;
A5: [d1,d2] `2 = d2 ;
thus (root-tree [d1,d2]) `1 = root-tree (((root-tree [d1,d2]) `1) . r) by A1, Th5
.= root-tree d1 by A3, A4, TREES_3:39 ; :: 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, Th5
.= root-tree d2 by A3, A5, TREES_3:39 ; :: thesis: verum