consider s being Element of S, x being set such that
x in X . s and
A6: t = [x,s] by A1, Th4;
reconsider f = F . s as Function ;
let a, b be Element of Union A; :: thesis: ( ( for f being Function st f = F . (t `2) holds
a = f . (root-tree t) ) & ( for f being Function st f = F . (t `2) holds
b = f . (root-tree t) ) implies a = b )
assume that
A7: for f being Function st f = F . (t `2) holds
a = f . (root-tree t) and
A8: for f being Function st f = F . (t `2) holds
b = f . (root-tree t) ; :: thesis: a = b
A9: f = F . (t `2) by A6;
then a = f . (root-tree t) by A7;
hence a = b by A8, A9; :: thesis: verum