let v1, v2 be Function of PL-WFF,BOOLEAN; :: thesis: ( v1 . FaLSUM = 0 & ( for k being Element of NAT holds
( v1 . (Prop k) = 1 iff Prop k in M ) ) & ( for p, q being Element of PL-WFF holds v1 . (p => q) = (v1 . p) => (v1 . q) ) & v2 . FaLSUM = 0 & ( for k being Element of NAT holds
( v2 . (Prop k) = 1 iff Prop k in M ) ) & ( for p, q being Element of PL-WFF holds v2 . (p => q) = (v2 . p) => (v2 . q) ) implies v1 = v2 )
assume A65: ( v1 . FaLSUM = 0 & ( for k being Element of NAT holds
( v1 . (Prop k) = 1 iff Prop k in M ) ) & ( for p, q being Element of PL-WFF holds v1 . (p => q) = (v1 . p) => (v1 . q) ) ) ; :: thesis: ( not v2 . FaLSUM = 0 or ex k being Element of NAT st
( ( v2 . (Prop k) = 1 implies Prop k in M ) implies ( Prop k in M & not v2 . (Prop k) = 1 ) ) or ex p, q being Element of PL-WFF st not v2 . (p => q) = (v2 . p) => (v2 . q) or v1 = v2 )
assume A66: ( v2 . FaLSUM = 0 & ( for k being Element of NAT holds
( v2 . (Prop k) = 1 iff Prop k in M ) ) & ( for p, q being Element of PL-WFF holds v2 . (p => q) = (v2 . p) => (v2 . q) ) ) ; :: thesis: v1 = v2
defpred S₁[ Element of PL-WFF ] means v1 . $1 = v2 . $1;
A67: for n being Element of NAT holds S₁[ Prop n]

proof

let n be Element of NAT ; :: thesis: S₁[ Prop n]

per cases ( Prop n in M or not Prop n in M ) ;

suppose A68: Prop n in M ; :: thesis: S₁[ Prop n]

hence v1 . (Prop n) = 1 by A65
.= v2 . (Prop n) by A66, A68 ;
:: thesis: verum

end;

suppose A69: not Prop n in M ; :: thesis: S₁[ Prop n]

then v1 . (Prop n) = 0 by XBOOLEAN:def 3, A65;
hence v1 . (Prop n) = v2 . (Prop n) by XBOOLEAN:def 3, A66, A69; :: thesis: verum

end;

end;

end;

A70: for p, q being Element of PL-WFF st S₁[p] & S₁[q] holds
S₁[p => q]

proof

let p, q be Element of PL-WFF ; :: thesis: ( S₁[p] & S₁[q] implies S₁[p => q] )
assume that
A71: S₁[p] and
A72: S₁[q] ; :: thesis: S₁[p => q]
thus v1 . (p => q) = (v1 . p) => (v1 . q) by A65
.= v2 . (p => q) by A66, A72, A71 ; :: thesis: verum

end;

A83: S₁[ FaLSUM ] by A66, A65;
for A being Element of PL-WFF holds S₁[A] from PL_AXIOM:sch 1(A83, A67, A70);
then A85: for x being Element of PL-WFF st x in dom v1 holds
v1 . x = v2 . x ;
dom v1 = PL-WFF by FUNCT_2:def 1
.= dom v2 by FUNCT_2:def 1 ;
hence v1 = v2 by A85, PARTFUN1:5; :: thesis: verum