let S be non empty non void ManySortedSign ; :: thesis: for X being V2() ManySortedSet of the carrier of S

for A being b_{1},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 V2() 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 ;

for A being b

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 V2() 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

hence
vf x = s -singleton x
; :: thesis: verum(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

end;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
(vf x) . y = (s -singleton x) . y
by A4, Def11; :: thesis: verum
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 }

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;proof

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 } )
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;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

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