let M1, M2 be ManySortedSet of HP-WFF ; :: 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 p9, q9 being DecoratedTree of HP-WFF st
( p9 = M1 . p & q9 = M1 . q & M1 . (p '&' q) = (p '&' q) -tree (p9,q9) & M1 . (p => q) = (p => q) -tree (p9,q9) ) ) & 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 p9, q9 being DecoratedTree of HP-WFF st
( p9 = M2 . p & q9 = M2 . q & M2 . (p '&' q) = (p '&' q) -tree (p9,q9) & M2 . (p => q) = (p => q) -tree (p9,q9) ) ) implies M1 = M2 )
assume that
A17: M1 . VERUM = root-tree VERUM and
A18: for n being Element of NAT holds M1 . (prop n) = root-tree (prop n) and
A19: for p, q being Element of HP-WFF ex p9, q9 being DecoratedTree of HP-WFF st
( p9 = M1 . p & q9 = M1 . q & M1 . (p '&' q) = (p '&' q) -tree (p9,q9) & M1 . (p => q) = (p => q) -tree (p9,q9) ) and
A20: M2 . VERUM = root-tree VERUM and
A21: for n being Element of NAT holds M2 . (prop n) = root-tree (prop n) and
A22: for p, q being Element of HP-WFF ex p9, q9 being DecoratedTree of HP-WFF st
( p9 = M2 . p & q9 = M2 . q & M2 . (p '&' q) = (p '&' q) -tree (p9,q9) & M2 . (p => q) = (p => q) -tree (p9,q9) ) ; :: thesis: M1 = M2
defpred S1[ Element of HP-WFF ] means M1 . $1 = M2 . $1;
A23: for n being Element of NAT holds S1[ prop n]
proof
let n be Element of NAT ; :: thesis: S1[ prop n]
thus M1 . (prop n) = root-tree (prop n) by A18
.= M2 . (prop n) by A21 ; :: thesis: verum
end;
A24: for r, s being Element of HP-WFF st S1[r] & S1[s] holds
( S1[r '&' s] & S1[r => s] )
proof
let r, s be Element of HP-WFF ; :: thesis: ( S1[r] & S1[s] implies ( S1[r '&' s] & S1[r => s] ) )
assume A25: ( M1 . r = M2 . r & M1 . s = M2 . s ) ; :: thesis: ( S1[r '&' s] & S1[r => s] )
A26: ( ex p9, q9 being DecoratedTree of HP-WFF st
( p9 = M1 . r & q9 = M1 . s & M1 . (r '&' s) = (r '&' s) -tree (p9,q9) & M1 . (r => s) = (r => s) -tree (p9,q9) ) & ex p9, q9 being DecoratedTree of HP-WFF st
( p9 = M2 . r & q9 = M2 . s & M2 . (r '&' s) = (r '&' s) -tree (p9,q9) & M2 . (r => s) = (r => s) -tree (p9,q9) ) ) by A19, A22;
hence M1 . (r '&' s) = M2 . (r '&' s) by A25; :: thesis: S1[r => s]
thus S1[r => s] by A25, A26; :: thesis: verum
end;
A27: S1[ VERUM ] by A17, A20;
for r being Element of HP-WFF holds S1[r] from HILBERT2:sch 2(A27, A23, A24);
 then for r being object st r in HP-WFF holds
M1 . r = M2 . r ;
hence M1 = M2 by PBOOLE:3; :: thesis: verum