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 p' being Permutation of (SetVal V,p) ex q' being Permutation of (SetVal V,q) st
( p' = M1 . p & q' = M1 . q & M1 . (p '&' q) = [:p',q':] & M1 . (p => q) = p' => q' ) ) & 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 p' being Permutation of (SetVal V,p) ex q' being Permutation of (SetVal V,q) st
( p' = M2 . p & q' = M2 . q & M2 . (p '&' q) = [:p',q':] & M2 . (p => q) = p' => q' ) ) 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 p' being Permutation of (SetVal V,p) ex q' being Permutation of (SetVal V,q) st
( p' = M1 . p & q' = M1 . q & M1 . (p '&' q) = [:p',q':] & M1 . (p => q) = p' => q' ) 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 p' being Permutation of (SetVal V,p) ex q' being Permutation of (SetVal V,q) st
( p' = M2 . p & q' = M2 . q & M2 . (p '&' q) = [:p',q':] & M2 . (p => q) = p' => q' ) ; :: thesis: M1 = M2
defpred S₁[ Element of HP-WFF ] means M1 . $1 = M2 . $1;
A28: S₁[ VERUM ] by A22, A25;
A29: for n being Element of NAT holds S₁[ prop n]

proof

let n be Element of NAT ; :: thesis: S₁[ prop n]
thus M1 . (prop n) = P . n by A23
.= M2 . (prop n) by A26 ; :: thesis: verum

end;

A30: for r, s being Element of HP-WFF st S₁[r] & S₁[s] holds
( S₁[r '&' s] & S₁[r => s] )

proof

let r, s be Element of HP-WFF ; :: thesis: ( S₁[r] & S₁[s] implies ( S₁[r '&' s] & S₁[r => s] ) )
assume A31: ( M1 . r = M2 . r & M1 . s = M2 . s ) ; :: thesis: ( S₁[r '&' s] & S₁[r => s] )
consider p' being Permutation of (SetVal V,r), q' being Permutation of (SetVal V,s) such that
A32: ( p' = M1 . r & q' = M1 . s ) and
A33: M1 . (r '&' s) = [:p',q':] and
A34: M1 . (r => s) = p' => q' by A24;
consider p' being Permutation of (SetVal V,r), q' being Permutation of (SetVal V,s) such that
A35: ( p' = M2 . r & q' = M2 . s ) and
A36: M2 . (r '&' s) = [:p',q':] and
A37: M2 . (r => s) = p' => q' by A27;
thus M1 . (r '&' s) = M2 . (r '&' s) by A31, A32, A33, A35, A36; :: thesis: S₁[r => s]
thus S₁[r => s] by A31, A32, A34, A35, A37; :: thesis: verum

end;

for r being Element of HP-WFF holds S₁[r] from HILBERT2:sch 2(A28, A29, A30);
then for r being set st r in HP-WFF holds
M1 . r = M2 . r ;
hence M1 = M2 by PBOOLE:3; :: thesis: verum