let M1, M2 be ManySortedSet of ; :: thesis: ( M1 . VERUM = root-tree VERUM & ( for n being Element of NAT holds M1 . (prop n) = root-tree (prop n) ) & ( for p, q being Element of HP-WFF ex p', q' being DecoratedTree of st
( p' = M1 . p & q' = M1 . q & M1 . (p '&' q) = (p '&' q) -tree p',q' & M1 . (p => q) = (p => q) -tree p',q' ) ) & M2 . VERUM = root-tree VERUM & ( for n being Element of NAT holds M2 . (prop n) = root-tree (prop n) ) & ( for p, q being Element of HP-WFF ex p', q' being DecoratedTree of st
( p' = M2 . p & q' = M2 . q & M2 . (p '&' q) = (p '&' q) -tree p',q' & M2 . (p => q) = (p => q) -tree p',q' ) ) implies M1 = M2 )
assume that
A18: M1 . VERUM = root-tree VERUM and
A19: for n being Element of NAT holds M1 . (prop n) = root-tree (prop n) and
A20: for p, q being Element of HP-WFF ex p', q' being DecoratedTree of st
( p' = M1 . p & q' = M1 . q & M1 . (p '&' q) = (p '&' q) -tree p',q' & M1 . (p => q) = (p => q) -tree p',q' ) and
A21: M2 . VERUM = root-tree VERUM and
A22: for n being Element of NAT holds M2 . (prop n) = root-tree (prop n) and
A23: for p, q being Element of HP-WFF ex p', q' being DecoratedTree of st
( p' = M2 . p & q' = M2 . q & M2 . (p '&' q) = (p '&' q) -tree p',q' & M2 . (p => q) = (p => q) -tree p',q' ) ; :: thesis: M1 = M2
defpred S₁[ Element of HP-WFF ] means M1 . $1 = M2 . $1;
A24: S₁[ VERUM ] by A18, A21;
A25: 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) = root-tree (prop n) by A19
.= M2 . (prop n) by A22 ; :: thesis: verum

end;

A26: 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 A27: ( M1 . r = M2 . r & M1 . s = M2 . s ) ; :: thesis: ( S₁[r '&' s] & S₁[r => s] )
consider p', q' being DecoratedTree of such that
A28: ( p' = M1 . r & q' = M1 . s ) and
A29: M1 . (r '&' s) = (r '&' s) -tree p',q' and
A30: M1 . (r => s) = (r => s) -tree p',q' by A20;
consider p', q' being DecoratedTree of such that
A31: ( p' = M2 . r & q' = M2 . s ) and
A32: M2 . (r '&' s) = (r '&' s) -tree p',q' and
A33: M2 . (r => s) = (r => s) -tree p',q' by A23;
thus M1 . (r '&' s) = M2 . (r '&' s) by A27, A28, A29, A31, A32; :: thesis: S₁[r => s]
thus S₁[r => s] by A27, A28, A30, A31, A33; :: thesis: verum

end;

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