let A be Element of LTLB_WFF ; :: thesis: for n being Element of NAT
for M being LTLModel
for f being Function of LTLB_WFF,BOOLEAN st ( for B being object st B in LTLB_WFF holds
f . B = (SAT M) . [n,B] ) holds
(VAL f) . A = (SAT M) . [n,A]
let n be Element of NAT ; :: thesis: for M being LTLModel
for f being Function of LTLB_WFF,BOOLEAN st ( for B being object st B in LTLB_WFF holds
f . B = (SAT M) . [n,B] ) holds
(VAL f) . A = (SAT M) . [n,A]
let M be LTLModel; :: thesis: for f being Function of LTLB_WFF,BOOLEAN st ( for B being object st B in LTLB_WFF holds
f . B = (SAT M) . [n,B] ) holds
(VAL f) . A = (SAT M) . [n,A]
let f be Function of LTLB_WFF,BOOLEAN; :: thesis: ( ( for B being object st B in LTLB_WFF holds
f . B = (SAT M) . [n,B] ) implies (VAL f) . A = (SAT M) . [n,A] )
defpred S₁[ Element of LTLB_WFF ] means (VAL f) . $1 = (SAT M) . [n,$1];
assume A1: for B being object st B in LTLB_WFF holds
f . B = (SAT M) . [n,B] ; :: thesis: (VAL f) . A = (SAT M) . [n,A]
A2: for k being Element of NAT holds S₁[ prop k]

proof

let k be Element of NAT ; :: thesis: S₁[ prop k]
(SAT M) . [n,(prop k)] = f . (prop k) by A1
.= (VAL f) . (prop k) by Def15 ;
hence S₁[ prop k] ; :: thesis: verum

end;

A3: for r, s being Element of LTLB_WFF st S₁[r] & S₁[s] holds
( S₁[r 'U' s] & S₁[r => s] )

proof

let r, s be Element of LTLB_WFF ; :: thesis: ( S₁[r] & S₁[s] implies ( S₁[r 'U' s] & S₁[r => s] ) )
assume A4: ( S₁[r] & S₁[s] ) ; :: thesis: ( S₁[r 'U' s] & S₁[r => s] )
(VAL f) . (r 'U' s) = f . (r 'U' s) by Def15
.= (SAT M) . [n,(r 'U' s)] by A1 ;
hence S₁[r 'U' s] ; :: thesis: S₁[r => s]
(SAT M) . [n,(r => s)] = ((SAT M) . [n,r]) => ((SAT M) . [n,s]) by Def11
.= (VAL f) . (r => s) by A4, Def15 ;
hence S₁[r => s] ; :: thesis: verum

end;

(SAT M) . [n,TFALSUM] = 0 by Def11
.= (VAL f) . TFALSUM by Def15 ;
then A5: S₁[ TFALSUM ] ;
for r being Element of LTLB_WFF holds S₁[r] from HILBERT2:sch 2(A5, A2, A3);
hence (VAL f) . A = (SAT M) . [n,A] ; :: thesis: verum