set bltl = bool LTLB_WFF;
let v1, v2 be Function of LTLB_WFF,(); :: thesis: ( ( for A, B being Element of LTLB_WFF
for n being Element of NAT holds
( v1 . 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 = & 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 = & 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 = & 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 = & 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 ;
hence ( S1[r 'U' s] & S1[r => s] ) by A19; :: thesis: verum
end;
A20: S1[ TFALSUM ] by ;
for x being Element of LTLB_WFF holds S1[x] from 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 ; :: thesis: verum
end;