defpred S₁[ Element of NAT , Element of BOOLEAN ] means ( $2 = 1 iff Prop $1 in M );
A16: for x being Element of NAT ex y being Element of BOOLEAN st S₁[x,y]

proof

let x be Element of NAT ; :: thesis: ex y being Element of BOOLEAN st S₁[x,y]
defpred S₂[ Element of BOOLEAN ] means ( $1 = 1 iff Prop x in M );

per cases ( prop x in M or not prop x in M ) ;

suppose prop x in M ; :: thesis: ex y being Element of BOOLEAN st S₁[x,y]

then S₂[ TRUE ] ;
hence ex y being Element of BOOLEAN st S₁[x,y] ; :: thesis: verum

end;

suppose not prop x in M ; :: thesis: ex y being Element of BOOLEAN st S₁[x,y]

then S₂[ FALSE ] ;
hence ex y being Element of BOOLEAN st S₁[x,y] ; :: thesis: verum

end;

end;

end;

consider f1 being sequence of BOOLEAN such that
A19: for k being Element of NAT holds S₁[k,f1 . k] from FUNCT_2:sch 3(A16);
deffunc H₁( Element of NAT ) -> Element of BOOLEAN = f1 . $1;
defpred S₂[ Element of HP-WFF , Element of HP-WFF , set , set , set ] means ex s5 being Element of BOOLEAN st $5 = FALSE ;
defpred S₃[ Element of HP-WFF , Element of HP-WFF , set , set , set ] means ( ( $3 is Element of BOOLEAN & $4 is Element of BOOLEAN implies ex s3, s4, s5 being Element of BOOLEAN st
( s3 = $3 & s4 = $4 & s5 = $5 & s5 = s3 => s4 ) ) & ( ( not $3 is Element of BOOLEAN or not $4 is Element of BOOLEAN ) implies $5 = FALSE ) );
A1: for p, q being Element of HP-WFF
for a, b being set ex c being set st S₂[p,q,a,b,c] ;
A2: for p, q being Element of HP-WFF
for a, b being set ex d being set st S₃[p,q,a,b,d]

proof

let p, q be Element of HP-WFF ; :: thesis: for a, b being set ex d being set st S₃[p,q,a,b,d]
let a, b be set ; :: thesis: ex d being set st S₃[p,q,a,b,d]

per cases ( ( a is Element of BOOLEAN & b is Element of BOOLEAN ) or not a is Element of BOOLEAN or not b is Element of BOOLEAN ) ;

suppose ( a is Element of BOOLEAN & b is Element of BOOLEAN ) ; :: thesis: ex d being set st S₃[p,q,a,b,d]

then reconsider a1 = a, b1 = b as Element of BOOLEAN ;
reconsider ab = a1 => b1 as Element of BOOLEAN by MARGREL1:def 12;
ab = a1 => b1 ;
hence ex d being set st S₃[p,q,a,b,d] ; :: thesis: verum

end;

suppose ( not a is Element of BOOLEAN or not b is Element of BOOLEAN ) ; :: thesis: ex d being set st S₃[p,q,a,b,d]

hence ex d being set st S₃[p,q,a,b,d] ; :: thesis: verum

end;

end;

end;

A3: for p, q being Element of HP-WFF
for a, b, c, d being set st S₂[p,q,a,b,c] & S₂[p,q,a,b,d] holds
c = d ;
A4: for p, q being Element of HP-WFF
for a, b, c, d being set st S₃[p,q,a,b,c] & S₃[p,q,a,b,d] holds
c = d ;
consider sat being ManySortedSet of HP-WFF such that
A34: ( sat . VERUM = 0 & ( for n being Element of NAT holds sat . (prop n) = H₁(n) ) & ( for p, q being Element of HP-WFF holds
( S₂[p,q,sat . p,sat . q,sat . (p '&' q)] & S₃[p,q,sat . p,sat . q,sat . (p => q)] ) ) ) from HILBERT2:sch 3(A1, A2, A3, A4);
A35: for x being object st x in HP-WFF holds
sat . x in BOOLEAN

proof

let x be object ; :: thesis: ( x in HP-WFF implies sat . x in BOOLEAN )
assume x in HP-WFF ; :: thesis: sat . x in BOOLEAN
then reconsider x1 = x as Element of HP-WFF ;

A42: now :: thesis: for n being Element of NAT holds sat . (prop n) in BOOLEAN

let n be Element of NAT ; :: thesis: sat . (prop n) in BOOLEAN
sat . (prop n) = f1 . n by A34;
hence sat . (prop n) in BOOLEAN ; :: thesis: verum

end;

per cases ( x1 = VERUM or x1 is simple or x1 is conjunctive or x1 is conditional ) by HILBERT2:9;

suppose x1 = VERUM ; :: thesis: sat . x in BOOLEAN

hence sat . x in BOOLEAN by A34; :: thesis: verum

end;

suppose x1 is simple ; :: thesis: sat . x in BOOLEAN

then ex n being Element of NAT st x1 = prop n by HILBERT2:def 8;
hence sat . x in BOOLEAN by A42; :: thesis: verum

end;

suppose x1 is conjunctive ; :: thesis: sat . x in BOOLEAN

then consider A, B being Element of HP-WFF such that
E2: x1 = A '&' B by HILBERT2:def 6;
consider s5 being Element of BOOLEAN such that
E3: sat . (A '&' B) = FALSE by A34;
thus sat . x in BOOLEAN by E3, E2; :: thesis: verum

end;

suppose x1 is conditional ; :: thesis: sat . x in BOOLEAN

then consider A, B being Element of HP-WFF such that
E1: x1 = A => B by HILBERT2:def 7;
A37: S₃[A,B,sat . A,sat . B,sat . (A => B)] by A34;
thus sat . x in BOOLEAN by A37, E1; :: thesis: verum

end;

end;

end;

dom sat = HP-WFF by PARTFUN1:def 2;
then reconsider sat = sat as Function of HP-WFF,BOOLEAN by A35, FUNCT_2:3;
set satc = sat | PL-WFF;
reconsider satc = sat | PL-WFF as Function of PL-WFF,BOOLEAN by FUNCT_2:32, plhp;
B1: satc . FaLSUM = 0 by A34, FUNCT_1:49;
B2: for k being Element of NAT holds
( satc . (Prop k) = 1 iff Prop k in M )

proof

let k be Element of NAT ; :: thesis: ( satc . (Prop k) = 1 iff Prop k in M )

hereby :: thesis: ( Prop k in M implies satc . (Prop k) = 1 )

assume satc . (Prop k) = 1 ; :: thesis: Prop k in M
then D2: sat . (Prop k) = 1 by FUNCT_1:49;
sat . (prop k) = f1 . k by A34;
hence Prop k in M by A19, D2; :: thesis: verum

end;

assume Prop k in M ; :: thesis: satc . (Prop k) = 1
then D1: f1 . k = 1 by A19;
sat . (prop k) = f1 . k by A34;
hence satc . (Prop k) = 1 by D1, FUNCT_1:49; :: thesis: verum

end;

for p, q being Element of PL-WFF holds satc . (p => q) = (satc . p) => (satc . q)

proof

let p, q be Element of PL-WFF ; :: thesis: satc . (p => q) = (satc . p) => (satc . q)
reconsider p1 = p, q1 = q as Element of HP-WFF by plhp;
consider s3, s4, s5 being Element of BOOLEAN such that
D4: ( s3 = sat . p1 & s4 = sat . q1 & s5 = sat . (p1 => q1) & s5 = s3 => s4 ) by A34;
thus satc . (p => q) = sat . (p => q) by FUNCT_1:49
.= (satc . p) => (sat . q) by FUNCT_1:49, D4
.= (satc . p) => (satc . q) by FUNCT_1:49 ; :: thesis: verum

end;

hence ex b₁ being Function of PL-WFF,BOOLEAN st
( b₁ . FaLSUM = 0 & ( for k being Element of NAT holds
( b₁ . (Prop k) = 1 iff Prop k in M ) ) & ( for p, q being Element of PL-WFF holds b₁ . (p => q) = (b₁ . p) => (b₁ . q) ) ) by B1, B2; :: thesis: verum