let v1, v2 be Function of [:NAT,LTLB_WFF:],BOOLEAN; :: thesis:
assume A65: for n being Element of NAT holds
( v1 . [n,TFALSUM] = 0 & ( for k being Element of NAT holds
( v1 . [n,(prop k)] = 1 iff prop k in M . n ) ) & ( for p, q being Element of LTLB_WFF holds
( v1 . [n,(p => q)] = (v1 . [n,p]) => (v1 . [n,q]) & ( v1 . [n,(p 'U' q)] = 1 implies ex i being Element of NAT st
( 0 < i & v1 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds
v1 . [(n + j),p] = 1 ) ) ) & ( ex i being Element of NAT st
( 0 < i & v1 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds
v1 . [(n + j),p] = 1 ) ) implies v1 . [n,(p 'U' q)] = 1 ) ) ) ) ; :: thesis:
assume A66: for n being Element of NAT holds
( v2 . [n,TFALSUM] = 0 & ( for k being Element of NAT holds
( v2 . [n,(prop k)] = 1 iff prop k in M . n ) ) & ( for p, q being Element of LTLB_WFF holds
( v2 . [n,(p => q)] = (v2 . [n,p]) => (v2 . [n,q]) & ( v2 . [n,(p 'U' q)] = 1 implies ex i being Element of NAT st
( 0 < i & v2 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds
v2 . [(n + j),p] = 1 ) ) ) & ( ex i being Element of NAT st
( 0 < i & v2 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds
v2 . [(n + j),p] = 1 ) ) implies v2 . [n,(p 'U' q)] = 1 ) ) ) ) ; :: thesis:
thus v1 = v2 :: thesis:

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

let k be Element of NAT ; :: thesis:

now :: thesis:

let n be Element of NAT ; :: thesis:

per cases ;

suppose A68: prop k in M . n ; :: thesis:

hence v1 . [n,(prop k)] = 1 by A65
.= v2 . [n,(prop k)] by A66, A68 ;
:: thesis:

end;

suppose A69: not prop k in M . n ; :: thesis:

then v1 . [n,(prop k)] = 0 by XBOOLEAN:def 3, A65;
hence v1 . [n,(prop k)] = v2 . [n,(prop k)] by XBOOLEAN:def 3, A66, A69; :: thesis:

end;

hence S₁[ prop k] ; :: thesis:

end;

A70: for p, q being Element of LTLB_WFF st S₁[p] & S₁[q] holds
( S₁[p 'U' q] & S₁[p => q] )

proof

let p, q be Element of LTLB_WFF ; :: thesis:
assume that
A71: S₁[p] and
A72: S₁[q] ; :: thesis:
thus S₁[p 'U' q] :: thesis:

proof

let n be Element of NAT ; :: thesis:

per cases ;

suppose A73: ex i being Element of NAT st
( 0 < i & v1 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds
v1 . [(n + j),p] = 1 ) ) ; :: thesis:

then consider i being Element of NAT such that
A74: 0 < i and
A75: v1 . [(n + i),q] = 1 and
A76: for j being Element of NAT st 1 <= j & j < i holds
v1 . [(n + j),p] = 1 ;
A77: v2 . [(n + i),q] = 1 by A72, A75;

A78: now :: thesis:

let j be Element of NAT ; :: thesis:
assume ( 1 <= j & j < i ) ; :: thesis:
then v1 . [(n + j),p] = 1 by A76;
hence v2 . [(n + j),p] = 1 by A71; :: thesis:

end;

thus v1 . [n,(p 'U' q)] = 1 by A65, A73
.= v2 . [n,(p 'U' q)] by A66, A74, A77, A78 ; :: thesis:

end;

suppose A79: for i being Element of NAT holds
( not 0 < i or not v1 . [(n + i),q] = 1 or ex j being Element of NAT st
( 1 <= j & j < i & not v1 . [(n + j),p] = 1 ) ) ; :: thesis:

A80: now :: thesis:

let i be Element of NAT ; :: thesis:

per cases by A79;

suppose not 0 < i ; :: thesis:

hence ( not 0 < i or not v2 . [(n + i),q] = 1 or ex j being Element of NAT st
( 1 <= j & j < i & not v2 . [(n + j),p] = 1 ) ) ; :: thesis:

end;

suppose not v1 . [(n + i),q] = 1 ; :: thesis:

hence ( not 0 < i or not v2 . [(n + i),q] = 1 or ex j being Element of NAT st
( 1 <= j & j < i & not v2 . [(n + j),p] = 1 ) ) by A72; :: thesis:

end;

suppose ex j being Element of NAT st
( 1 <= j & j < i & not v1 . [(n + j),p] = 1 ) ; :: thesis:

then consider j being Element of NAT such that
A81: ( 1 <= j & j < i ) and
A82: not v1 . [(n + j),p] = 1 ;
not v2 . [(n + j),p] = 1 by A71, A82;
hence ( not 0 < i or not v2 . [(n + i),q] = 1 or ex j being Element of NAT st
( 1 <= j & j < i & not v2 . [(n + j),p] = 1 ) ) by A81; :: thesis:

end;

v1 . [n,(p 'U' q)] = 0 by XBOOLEAN:def 3, A65, A79;
hence v1 . [n,(p 'U' q)] = v2 . [n,(p 'U' q)] by A66, XBOOLEAN:def 3, A80; :: thesis:

end;

thus S₁[p => q] :: thesis:

proof

let n be Element of NAT ; :: thesis:
thus v1 . [n,(p => q)] = (v1 . [n,p]) => (v1 . [n,q]) by A65
.= (v2 . [n,p]) => (v1 . [n,q]) by A71
.= (v2 . [n,p]) => (v2 . [n,q]) by A72
.= v2 . [n,(p => q)] by A66 ; :: thesis:

end;

now :: thesis:

let n be Element of NAT ; :: thesis:
thus v1 . [n,TFALSUM] = 0 by A65
.= v2 . [n,TFALSUM] by A66 ; :: thesis:

end;

then A83: S₁[ TFALSUM ] ;
A84: for A being Element of LTLB_WFF holds S₁[A] from HILBERT2:sch 2(A83, A67, A70);
A85: for x being Element of [:NAT,LTLB_WFF:] st x in dom v1 holds
v1 . x = v2 . x

proof

let x be Element of [:NAT,LTLB_WFF:]; :: thesis:
consider y, z being object such that
A86: y in NAT and
A87: z in LTLB_WFF and
A88: x = [y,z] by ZFMISC_1:def 2;
reconsider y1 = y as Element of NAT by A86;
assume x in dom v1 ; :: thesis:
thus v1 . x = v2 . x by A84, A86, A87, A88; :: thesis:
reconsider z1 = z as Element of LTLB_WFF by A87;

end;

dom v1 = [:NAT,LTLB_WFF:] by FUNCT_2:def 1
.= dom v2 by FUNCT_2:def 1 ;
hence v1 = v2 by A85, PARTFUN1:5; :: thesis:

end;