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) = ((tau1 . (untn (A,B))) \/ (v1 . A)) \/ (v1 . 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) = ((tau1 . (untn (A,B))) \/ (v2 . A)) \/ (v2 . B) ) ) implies v1 = v2 )
assume A17: 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) = ((tau1 . (untn (A,B))) \/ (v1 . A)) \/ (v1 . 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) = ((tau1 . (untn (A,B))) \/ (v2 . A)) \/ (v2 . B) ) or v1 = v2 )
assume A18: 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) = ((tau1 . (untn (A,B))) \/ (v2 . A)) \/ (v2 . B) ) ; :: thesis: v1 = v2
thus v1 = v2 :: thesis: verum

proof

defpred S₁[ Element of LTLB_WFF ] means v1 . $1 = v2 . $1;
A19: 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 A17
.= v2 . (prop n) by A18 ;
hence S₁[ prop n] ; :: thesis: verum

end;

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

end;

A23: S₁[ TFALSUM ] by A17, A18;
for x being Element of LTLB_WFF holds S₁[x] from HILBERT2:sch 2(A23, A19, A20);
then A24: 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 A24, PARTFUN1:5; :: thesis: verum

end;