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