set bltl = bool LTLB_WFF;
let v1, v2 be Function of LTLB_WFF,(bool LTLB_WFF); :: thesis: ( ( for A, B being Element of LTLB_WFF
for n being Element of NAT holds
( v1 . TFALSUM = {TFALSUM} & v1 . (prop n) = {(prop n)} & v1 . (A => B) = ({(A => B)} \/ (v1 . A)) \/ (v1 . B) & v1 . (A 'U' B) = {(A 'U' B)} ) ) & ( for A, B being Element of LTLB_WFF
for n being Element of NAT holds
( v2 . TFALSUM = {TFALSUM} & v2 . (prop n) = {(prop n)} & v2 . (A => B) = ({(A => B)} \/ (v2 . A)) \/ (v2 . B) & v2 . (A 'U' B) = {(A 'U' B)} ) ) implies v1 = v2 )
assume A14: for A, B being Element of LTLB_WFF
for n being Element of NAT holds
( v1 . TFALSUM = {TFALSUM} & v1 . (prop n) = {(prop n)} & v1 . (A => B) = ({(A => B)} \/ (v1 . A)) \/ (v1 . B) & v1 . (A 'U' B) = {(A 'U' B)} ) ; :: thesis: ( ex A, B being Element of LTLB_WFF ex n being Element of NAT st
( v2 . TFALSUM = {TFALSUM} & v2 . (prop n) = {(prop n)} & v2 . (A => B) = ({(A => B)} \/ (v2 . A)) \/ (v2 . B) implies not v2 . (A 'U' B) = {(A 'U' B)} ) or v1 = v2 )
assume A15: for A, B being Element of LTLB_WFF
for n being Element of NAT holds
( v2 . TFALSUM = {TFALSUM} & v2 . (prop n) = {(prop n)} & v2 . (A => B) = ({(A => B)} \/ (v2 . A)) \/ (v2 . B) & v2 . (A 'U' B) = {(A 'U' B)} ) ; :: thesis: v1 = v2
thus v1 = v2 :: thesis: verum

proof

defpred S₁[ Element of LTLB_WFF ] means v1 . $1 = v2 . $1;
A16: for n being Element of NAT holds S₁[ prop n]

proof

let n be Element of NAT ; :: thesis: S₁[ prop n]
v1 . (prop n) = {(prop n)} by A14
.= v2 . (prop n) by A15 ;
hence S₁[ prop n] ; :: thesis: verum

end;

A17: 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 A18: ( S₁[r] & S₁[s] ) ; :: thesis: ( S₁[r 'U' s] & S₁[r => s] )
A19: v1 . (r 'U' s) = {(r 'U' s)} by A14
.= v2 . (r 'U' s) by A15 ;
v1 . (r => s) = ({(r => s)} \/ (v1 . r)) \/ (v1 . s) by A14
.= v2 . (r => s) by A15, A18 ;
hence ( S₁[r 'U' s] & S₁[r => s] ) by A19; :: thesis: verum

end;

A20: S₁[ TFALSUM ] by A14, A15;
for x being Element of LTLB_WFF holds S₁[x] from HILBERT2:sch 2(A20, A16, A17);
then A21: for x being Element of LTLB_WFF st x in dom v1 holds
S₁[x] ;
dom v1 = LTLB_WFF by FUNCT_2:def 1
.= dom v2 by FUNCT_2:def 1 ;
hence v1 = v2 by A21, PARTFUN1:5; :: thesis: verum

end;