let f, f1 be FinSequence of LTLB_WFF ; :: thesis: for g being Function of LTLB_WFF,BOOLEAN st rng f = rng f1 holds
(VAL g) . ((con f) /. (len (con f))) = (VAL g) . ((con f1) /. (len (con f1)))
let g be Function of LTLB_WFF,BOOLEAN; :: thesis: ( rng f = rng f1 implies (VAL g) . ((con f) /. (len (con f))) = (VAL g) . ((con f1) /. (len (con f1))) )
set v = VAL g;
assume A1: rng f = rng f1 ; :: thesis: (VAL g) . ((con f) /. (len (con f))) = (VAL g) . ((con f1) /. (len (con f1)))

per cases ( len f = 0 or len f > 0 ) ;

suppose A2: len f = 0 ; :: thesis: (VAL g) . ((con f) /. (len (con f))) = (VAL g) . ((con f1) /. (len (con f1)))

then len f1 = 0 by Th3, A1;
then A3: f1 = {} ;
f = {} by A2;
hence (VAL g) . H₂(f) = (VAL g) . H₂(f1) by A3; :: thesis: verum

end;

suppose len f > 0 ; :: thesis: (VAL g) . ((con f) /. (len (con f))) = (VAL g) . ((con f1) /. (len (con f1)))

per cases ( (VAL g) . H₂(f) = 1 or (VAL g) . H₂(f) = 0 ) by XBOOLEAN:def 3;

suppose A4: (VAL g) . H₂(f) = 1 ; :: thesis: (VAL g) . ((con f) /. (len (con f))) = (VAL g) . ((con f1) /. (len (con f1)))

assume not (VAL g) . H₂(f) = (VAL g) . H₂(f1) ; :: thesis: contradiction
then consider i being Nat such that
A5: i in dom f1 and
A6: not (VAL g) . (f1 /. i) = 1 by A4, Th19;
set j = (f1 /. i) .. f;
f1 /. i in rng f by A5, PARTFUN2:2, A1;
then ( (f1 /. i) .. f in dom f & (VAL g) . (f /. ((f1 /. i) .. f)) = (VAL g) . (f1 /. i) ) by FINSEQ_4:20, FINSEQ_5:38;
hence contradiction by Th19, A4, A6; :: thesis: verum

end;

suppose A7: (VAL g) . H₂(f) = 0 ; :: thesis: (VAL g) . ((con f) /. (len (con f))) = (VAL g) . ((con f1) /. (len (con f1)))

assume A8: not (VAL g) . H₂(f) = (VAL g) . H₂(f1) ; :: thesis: contradiction
consider i being Nat such that
A9: i in dom f and
A10: not (VAL g) . (f /. i) = 1 by A7, Th19;
set j = (f /. i) .. f1;
A11: f /. i in rng f1 by A9, PARTFUN2:2, A1;
then (f /. i) .. f1 in dom f1 by FINSEQ_4:20;
then (VAL g) . (f1 /. ((f /. i) .. f1)) = 1 by Th19, A8, A7, XBOOLEAN:def 3;
hence contradiction by A10, FINSEQ_5:38, A11; :: thesis: verum

end;

end;

end;

end;