let S be non empty non void ManySortedSign ; :: thesis: for X being non-empty ManySortedSet of the carrier of S
for A being b₁,S -terms all_vars_including vf-free VarMSAlgebra over S
for s being SortSymbol of S
for x being Element of A,s st x in (FreeGen X) . s holds
vf x = s -singleton x
let X be non-empty ManySortedSet of the carrier of S; :: thesis: for A being X,S -terms all_vars_including vf-free VarMSAlgebra over S
for s being SortSymbol of S
for x being Element of A,s st x in (FreeGen X) . s holds
vf x = s -singleton x
let A be X,S -terms all_vars_including vf-free VarMSAlgebra over S; :: thesis: for s being SortSymbol of S
for x being Element of A,s st x in (FreeGen X) . s holds
vf x = s -singleton x
let s be SortSymbol of S; :: thesis: for x being Element of A,s st x in (FreeGen X) . s holds
vf x = s -singleton x
let x be Element of A,s; :: thesis: ( x in (FreeGen X) . s implies vf x = s -singleton x )
assume x in (FreeGen X) . s ; :: thesis: vf x = s -singleton x
then x in FreeGen (s,X) by MSAFREE:def 16;
then consider a being set such that
A1: ( a in X . s & x = root-tree [a,s] ) by MSAFREE:def 15;
A2: ( dom (root-tree [a,s]) = {{}} & (root-tree [a,s]) . {} = [a,s] ) by TREES_4:3, TREES_1:29;
A3: [a,s] `2 = s ;

now :: thesis: for y being object st y in the carrier of S holds
(vf x) . y = (s -singleton x) . y

let y be object ; :: thesis: ( y in the carrier of S implies (vf x) . y = (s -singleton x) . y )
assume y in the carrier of S ; :: thesis: (vf x) . y = (s -singleton x) . y
then reconsider r = y as SortSymbol of S ;
A4: { (x | p) where p is Element of dom x : ((x | p) . {}) `2 = r } = (s -singleton x) . y

proof

thus { (x | p) where p is Element of dom x : ((x | p) . {}) `2 = r } c= (s -singleton x) . y :: according to XBOOLE_0:def 10 :: thesis: (s -singleton x) . y c= { (x | p) where p is Element of dom x : ((x | p) . {}) `2 = r }

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in { (x | p) where p is Element of dom x : ((x | p) . {}) `2 = r } or z in (s -singleton x) . y )
assume z in { (x | p) where p is Element of dom x : ((x | p) . {}) `2 = r } ; :: thesis: z in (s -singleton x) . y
then consider p being Element of dom x such that
A5: ( z = x | p & ((x | p) . {}) `2 = r ) ;
p = {} by A1, A2;
then A6: z = x by A5, TREES_9:1;
then (s -singleton x) . r = {x} by A1, A2, A5, Th6;
hence z in (s -singleton x) . y by A6, TARSKI:def 1; :: thesis: verum

end;

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in (s -singleton x) . y or z in { (x | p) where p is Element of dom x : ((x | p) . {}) `2 = r } )
reconsider p = {} as Element of dom x by A1, A2, TARSKI:def 1;
assume A7: z in (s -singleton x) . y ; :: thesis: z in { (x | p) where p is Element of dom x : ((x | p) . {}) `2 = r }
then A8: r = s by Th6;
then z in {x} by A7, Th6;
then A9: z = x by TARSKI:def 1;
then z = x | p by TREES_9:1;
hence z in { (x | p) where p is Element of dom x : ((x | p) . {}) `2 = r } by A1, A2, A3, A9, A8; :: thesis: verum

end;

thus (vf x) . y = (s -singleton x) . y by A4, Def11; :: thesis: verum

end;

hence vf x = s -singleton x ; :: thesis: verum