let M1, M2 be ManySortedFunction of SetVal V, SetVal V; :: thesis: ( M1 . VERUM = id 1 & ( for n being Element of NAT holds M1 . (prop n) = P . n ) & ( for p, q being Element of HP-WFF ex p9 being Permutation of (SetVal (V,p)) ex q9 being Permutation of (SetVal (V,q)) st

( p9 = M1 . p & q9 = M1 . q & M1 . (p '&' q) = [:p9,q9:] & M1 . (p => q) = p9 => q9 ) ) & M2 . VERUM = id 1 & ( for n being Element of NAT holds M2 . (prop n) = P . n ) & ( for p, q being Element of HP-WFF ex p9 being Permutation of (SetVal (V,p)) ex q9 being Permutation of (SetVal (V,q)) st

( p9 = M2 . p & q9 = M2 . q & M2 . (p '&' q) = [:p9,q9:] & M2 . (p => q) = p9 => q9 ) ) implies M1 = M2 )

assume that

A22: M1 . VERUM = id 1 and

A23: for n being Element of NAT holds M1 . (prop n) = P . n and

A24: for p, q being Element of HP-WFF ex p9 being Permutation of (SetVal (V,p)) ex q9 being Permutation of (SetVal (V,q)) st

( p9 = M1 . p & q9 = M1 . q & M1 . (p '&' q) = [:p9,q9:] & M1 . (p => q) = p9 => q9 ) and

A25: M2 . VERUM = id 1 and

A26: for n being Element of NAT holds M2 . (prop n) = P . n and

A27: for p, q being Element of HP-WFF ex p9 being Permutation of (SetVal (V,p)) ex q9 being Permutation of (SetVal (V,q)) st

( p9 = M2 . p & q9 = M2 . q & M2 . (p '&' q) = [:p9,q9:] & M2 . (p => q) = p9 => q9 ) ; :: thesis: M1 = M2

defpred S_{1}[ Element of HP-WFF ] means M1 . $1 = M2 . $1;

A28: for n being Element of NAT holds S_{1}[ prop n]
_{1}[r] & S_{1}[s] holds

( S_{1}[r '&' s] & S_{1}[r => s] )
_{1}[ VERUM ]
by A22, A25;

for r being Element of HP-WFF holds S_{1}[r]
from HILBERT2:sch 2(A32, A28, A29);

hence M1 = M2 ; :: thesis: verum

( p9 = M1 . p & q9 = M1 . q & M1 . (p '&' q) = [:p9,q9:] & M1 . (p => q) = p9 => q9 ) ) & M2 . VERUM = id 1 & ( for n being Element of NAT holds M2 . (prop n) = P . n ) & ( for p, q being Element of HP-WFF ex p9 being Permutation of (SetVal (V,p)) ex q9 being Permutation of (SetVal (V,q)) st

( p9 = M2 . p & q9 = M2 . q & M2 . (p '&' q) = [:p9,q9:] & M2 . (p => q) = p9 => q9 ) ) implies M1 = M2 )

assume that

A22: M1 . VERUM = id 1 and

A23: for n being Element of NAT holds M1 . (prop n) = P . n and

A24: for p, q being Element of HP-WFF ex p9 being Permutation of (SetVal (V,p)) ex q9 being Permutation of (SetVal (V,q)) st

( p9 = M1 . p & q9 = M1 . q & M1 . (p '&' q) = [:p9,q9:] & M1 . (p => q) = p9 => q9 ) and

A25: M2 . VERUM = id 1 and

A26: for n being Element of NAT holds M2 . (prop n) = P . n and

A27: for p, q being Element of HP-WFF ex p9 being Permutation of (SetVal (V,p)) ex q9 being Permutation of (SetVal (V,q)) st

( p9 = M2 . p & q9 = M2 . q & M2 . (p '&' q) = [:p9,q9:] & M2 . (p => q) = p9 => q9 ) ; :: thesis: M1 = M2

defpred S

A28: for n being Element of NAT holds S

proof

A29:
for r, s being Element of HP-WFF st S
let n be Element of NAT ; :: thesis: S_{1}[ prop n]

thus M1 . (prop n) = P . n by A23

.= M2 . (prop n) by A26 ; :: thesis: verum

end;thus M1 . (prop n) = P . n by A23

.= M2 . (prop n) by A26 ; :: thesis: verum

( S

proof

A32:
S
let r, s be Element of HP-WFF ; :: thesis: ( S_{1}[r] & S_{1}[s] implies ( S_{1}[r '&' s] & S_{1}[r => s] ) )

assume A30: ( M1 . r = M2 . r & M1 . s = M2 . s ) ; :: thesis: ( S_{1}[r '&' s] & S_{1}[r => s] )

A31: ( ex p9 being Permutation of (SetVal (V,r)) ex q9 being Permutation of (SetVal (V,s)) st

( p9 = M1 . r & q9 = M1 . s & M1 . (r '&' s) = [:p9,q9:] & M1 . (r => s) = p9 => q9 ) & ex p9 being Permutation of (SetVal (V,r)) ex q9 being Permutation of (SetVal (V,s)) st

( p9 = M2 . r & q9 = M2 . s & M2 . (r '&' s) = [:p9,q9:] & M2 . (r => s) = p9 => q9 ) ) by A24, A27;

hence M1 . (r '&' s) = M2 . (r '&' s) by A30; :: thesis: S_{1}[r => s]

thus S_{1}[r => s]
by A30, A31; :: thesis: verum

end;assume A30: ( M1 . r = M2 . r & M1 . s = M2 . s ) ; :: thesis: ( S

A31: ( ex p9 being Permutation of (SetVal (V,r)) ex q9 being Permutation of (SetVal (V,s)) st

( p9 = M1 . r & q9 = M1 . s & M1 . (r '&' s) = [:p9,q9:] & M1 . (r => s) = p9 => q9 ) & ex p9 being Permutation of (SetVal (V,r)) ex q9 being Permutation of (SetVal (V,s)) st

( p9 = M2 . r & q9 = M2 . s & M2 . (r '&' s) = [:p9,q9:] & M2 . (r => s) = p9 => q9 ) ) by A24, A27;

hence M1 . (r '&' s) = M2 . (r '&' s) by A30; :: thesis: S

thus S

for r being Element of HP-WFF holds S

hence M1 = M2 ; :: thesis: verum