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

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