let v1, v2 be Function of LTLB_WFF,BOOLEAN; :: thesis: ( ( for A, B being Element of LTLB_WFF

for n being Element of NAT holds

( v1 . TFALSUM = 0 & v1 . (prop n) = f . (prop n) & v1 . (A => B) = (v1 . A) => (v1 . B) & v1 . (A 'U' B) = f . (A 'U' B) ) ) & ( for A, B being Element of LTLB_WFF

for n being Element of NAT holds

( v2 . TFALSUM = 0 & v2 . (prop n) = f . (prop n) & v2 . (A => B) = (v2 . A) => (v2 . B) & v2 . (A 'U' B) = f . (A 'U' B) ) ) implies v1 = v2 )

assume A17: for A, B being Element of LTLB_WFF

for n being Element of NAT holds

( v1 . TFALSUM = 0 & v1 . (prop n) = f . (prop n) & v1 . (A => B) = (v1 . A) => (v1 . B) & v1 . (A 'U' B) = f . (A 'U' B) ) ; :: thesis: ( ex A, B being Element of LTLB_WFF ex n being Element of NAT st

( v2 . TFALSUM = 0 & v2 . (prop n) = f . (prop n) & v2 . (A => B) = (v2 . A) => (v2 . B) implies not v2 . (A 'U' B) = f . (A 'U' B) ) or v1 = v2 )

assume A18: for A, B being Element of LTLB_WFF

for n being Element of NAT holds

( v2 . TFALSUM = 0 & v2 . (prop n) = f . (prop n) & v2 . (A => B) = (v2 . A) => (v2 . B) & v2 . (A 'U' B) = f . (A 'U' B) ) ; :: thesis: v1 = v2

thus v1 = v2 :: thesis: verum

for n being Element of NAT holds

( v1 . TFALSUM = 0 & v1 . (prop n) = f . (prop n) & v1 . (A => B) = (v1 . A) => (v1 . B) & v1 . (A 'U' B) = f . (A 'U' B) ) ) & ( for A, B being Element of LTLB_WFF

for n being Element of NAT holds

( v2 . TFALSUM = 0 & v2 . (prop n) = f . (prop n) & v2 . (A => B) = (v2 . A) => (v2 . B) & v2 . (A 'U' B) = f . (A 'U' B) ) ) implies v1 = v2 )

assume A17: for A, B being Element of LTLB_WFF

for n being Element of NAT holds

( v1 . TFALSUM = 0 & v1 . (prop n) = f . (prop n) & v1 . (A => B) = (v1 . A) => (v1 . B) & v1 . (A 'U' B) = f . (A 'U' B) ) ; :: thesis: ( ex A, B being Element of LTLB_WFF ex n being Element of NAT st

( v2 . TFALSUM = 0 & v2 . (prop n) = f . (prop n) & v2 . (A => B) = (v2 . A) => (v2 . B) implies not v2 . (A 'U' B) = f . (A 'U' B) ) or v1 = v2 )

assume A18: for A, B being Element of LTLB_WFF

for n being Element of NAT holds

( v2 . TFALSUM = 0 & v2 . (prop n) = f . (prop n) & v2 . (A => B) = (v2 . A) => (v2 . B) & v2 . (A 'U' B) = f . (A 'U' B) ) ; :: thesis: v1 = v2

thus v1 = v2 :: thesis: verum

proof

defpred S_{1}[ Element of LTLB_WFF ] means v1 . $1 = v2 . $1;

A19: for n being Element of NAT holds S_{1}[ prop n]
_{1}[r] & S_{1}[s] holds

( S_{1}[r 'U' s] & S_{1}[r => s] )
_{1}[ TFALSUM ]
by A17, A18;

for x being Element of LTLB_WFF holds S_{1}[x]
from HILBERT2:sch 2(A23, A19, A20);

then A24: for x being Element of LTLB_WFF st x in dom v1 holds

S_{1}[x]
;

dom v1 = LTLB_WFF by FUNCT_2:def 1

.= dom v2 by FUNCT_2:def 1 ;

hence v1 = v2 by A24, PARTFUN1:5; :: thesis: verum

end;A19: for n being Element of NAT holds S

proof

A20:
for r, s being Element of LTLB_WFF st S
let n be Element of NAT ; :: thesis: S_{1}[ prop n]

v1 . (prop n) = f . (prop n) by A17

.= v2 . (prop n) by A18 ;

hence S_{1}[ prop n]
; :: thesis: verum

end;v1 . (prop n) = f . (prop n) by A17

.= v2 . (prop n) by A18 ;

hence S

( S

proof

A23:
S
let r, s be Element of LTLB_WFF ; :: thesis: ( S_{1}[r] & S_{1}[s] implies ( S_{1}[r 'U' s] & S_{1}[r => s] ) )

assume A21: ( S_{1}[r] & S_{1}[s] )
; :: thesis: ( S_{1}[r 'U' s] & S_{1}[r => s] )

A22: v1 . (r 'U' s) = f . (r 'U' s) by A17

.= v2 . (r 'U' s) by A18 ;

v1 . (r => s) = (v1 . r) => (v1 . s) by A17

.= v2 . (r => s) by A18, A21 ;

hence ( S_{1}[r 'U' s] & S_{1}[r => s] )
by A22; :: thesis: verum

end;assume A21: ( S

A22: v1 . (r 'U' s) = f . (r 'U' s) by A17

.= v2 . (r 'U' s) by A18 ;

v1 . (r => s) = (v1 . r) => (v1 . s) by A17

.= v2 . (r => s) by A18, A21 ;

hence ( S

for x being Element of LTLB_WFF holds S

then A24: for x being Element of LTLB_WFF st x in dom v1 holds

S

dom v1 = LTLB_WFF by FUNCT_2:def 1

.= dom v2 by FUNCT_2:def 1 ;

hence v1 = v2 by A24, PARTFUN1:5; :: thesis: verum