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 S1[ Element of LTLB_WFF ] means v1 . $1 = v2 . $1;
A16: for n being Element of NAT holds S1[ prop n]
proof
let n be Element of NAT ; :: thesis: S1[ prop n]
v1 . (prop n) = {(prop n)} by A14
.= v2 . (prop n) by A15 ;
hence S1[ prop n] ; :: thesis: verum
end;
A17: for r, s being Element of LTLB_WFF st S1[r] & S1[s] holds
( S1[r 'U' s] & S1[r => s] )
proof
let r, s be Element of LTLB_WFF ; :: thesis: ( S1[r] & S1[s] implies ( S1[r 'U' s] & S1[r => s] ) )
assume A18: ( S1[r] & S1[s] ) ; :: thesis: ( S1[r 'U' s] & S1[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 ( S1[r 'U' s] & S1[r => s] ) by A19; :: thesis: verum
end;
A20: S1[ TFALSUM ] by A14, A15;
for x being Element of LTLB_WFF holds S1[x] from HILBERT2:sch 2(A20, A16, A17);
 then A21: for x being Element of LTLB_WFF st x in dom v1 holds
S1[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;