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₁[ Element of HP-WFF ] means M1 . $1 = M2 . $1;
A28: 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;

A29: 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 A30: ( M1 . r = M2 . r & M1 . s = M2 . s ) ; :: thesis: ( S₁[r '&' s] & S₁[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₁[r => s]
thus S₁[r => s] by A30, A31; :: thesis: verum

end;

A32: S₁[ VERUM ] by A22, A25;
for r being Element of HP-WFF holds S₁[r] from HILBERT2:sch 2(A32, A28, A29);
hence M1 = M2 ; :: thesis: verum