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
A6: for f being Function st f = F . (t `2 ) holds
a = f . (root-tree t) and
A7: for f being Function st f = F . (t `2 ) holds
b = f . (root-tree t) ; :: thesis: a = b
consider s being SortSymbol of S, x being set such that
A8: ( x in X . s & t = [x,s] ) by A1, Th7;
reconsider f = F . s as Function ;
f = F . (t `2 ) by A8, MCART_1:7;
then ( a = f . (root-tree t) & b = f . (root-tree t) ) by A6, A7;
hence a = b ; :: thesis: verum