let Al be QC-alphabet ; :: thesis: for r being Element of CQC-WFF Al
for A being non empty set
for Al2 being Al -expanding QC-alphabet
for J2 being interpretation of Al2,A
for Jp being interpretation of Al,A
for v2 being Element of Valuations_in (Al2,A)
for vp being Element of Valuations_in (Al,A) st Jp = J2 | () & vp = v2 | () holds
( J2,v2 |= Al2 -Cast r iff Jp,vp |= r )

let r be Element of CQC-WFF Al; :: thesis: for A being non empty set
for Al2 being Al -expanding QC-alphabet
for J2 being interpretation of Al2,A
for Jp being interpretation of Al,A
for v2 being Element of Valuations_in (Al2,A)
for vp being Element of Valuations_in (Al,A) st Jp = J2 | () & vp = v2 | () holds
( J2,v2 |= Al2 -Cast r iff Jp,vp |= r )

let A be non empty set ; :: thesis: for Al2 being Al -expanding QC-alphabet
for J2 being interpretation of Al2,A
for Jp being interpretation of Al,A
for v2 being Element of Valuations_in (Al2,A)
for vp being Element of Valuations_in (Al,A) st Jp = J2 | () & vp = v2 | () holds
( J2,v2 |= Al2 -Cast r iff Jp,vp |= r )

let Al2 be Al -expanding QC-alphabet ; :: thesis: for J2 being interpretation of Al2,A
for Jp being interpretation of Al,A
for v2 being Element of Valuations_in (Al2,A)
for vp being Element of Valuations_in (Al,A) st Jp = J2 | () & vp = v2 | () holds
( J2,v2 |= Al2 -Cast r iff Jp,vp |= r )

let J2 be interpretation of Al2,A; :: thesis: for Jp being interpretation of Al,A
for v2 being Element of Valuations_in (Al2,A)
for vp being Element of Valuations_in (Al,A) st Jp = J2 | () & vp = v2 | () holds
( J2,v2 |= Al2 -Cast r iff Jp,vp |= r )

let Jp be interpretation of Al,A; :: thesis: for v2 being Element of Valuations_in (Al2,A)
for vp being Element of Valuations_in (Al,A) st Jp = J2 | () & vp = v2 | () holds
( J2,v2 |= Al2 -Cast r iff Jp,vp |= r )

let v2 be Element of Valuations_in (Al2,A); :: thesis: for vp being Element of Valuations_in (Al,A) st Jp = J2 | () & vp = v2 | () holds
( J2,v2 |= Al2 -Cast r iff Jp,vp |= r )

let vp be Element of Valuations_in (Al,A); :: thesis: ( Jp = J2 | () & vp = v2 | () implies ( J2,v2 |= Al2 -Cast r iff Jp,vp |= r ) )
defpred S1[ Element of CQC-WFF Al] means for J2 being interpretation of Al2,A
for Jp being interpretation of Al,A
for v2 being Element of Valuations_in (Al2,A)
for vp being Element of Valuations_in (Al,A) st Jp = J2 | () & vp = v2 | () holds
( J2,v2 |= Al2 -Cast \$1 iff Jp,vp |= \$1 );
A1: S1[ VERUM Al]
proof
let J2 be interpretation of Al2,A; :: thesis: for Jp being interpretation of Al,A
for v2 being Element of Valuations_in (Al2,A)
for vp being Element of Valuations_in (Al,A) st Jp = J2 | () & vp = v2 | () holds
( J2,v2 |= Al2 -Cast (VERUM Al) iff Jp,vp |= VERUM Al )

let Jp be interpretation of Al,A; :: thesis: for v2 being Element of Valuations_in (Al2,A)
for vp being Element of Valuations_in (Al,A) st Jp = J2 | () & vp = v2 | () holds
( J2,v2 |= Al2 -Cast (VERUM Al) iff Jp,vp |= VERUM Al )

let v2 be Element of Valuations_in (Al2,A); :: thesis: for vp being Element of Valuations_in (Al,A) st Jp = J2 | () & vp = v2 | () holds
( J2,v2 |= Al2 -Cast (VERUM Al) iff Jp,vp |= VERUM Al )

let vp be Element of Valuations_in (Al,A); :: thesis: ( Jp = J2 | () & vp = v2 | () implies ( J2,v2 |= Al2 -Cast (VERUM Al) iff Jp,vp |= VERUM Al ) )
J2,v2 |= VERUM Al2 by VALUAT_1:32;
hence ( Jp = J2 | () & vp = v2 | () implies ( J2,v2 |= Al2 -Cast (VERUM Al) iff Jp,vp |= VERUM Al ) ) by VALUAT_1:32; :: thesis: verum
end;
A2: for k being Nat
for P being QC-pred_symbol of k,Al
for l being CQC-variable_list of k,Al holds S1[P ! l]
proof
let k be Nat; :: thesis: for P being QC-pred_symbol of k,Al
for l being CQC-variable_list of k,Al holds S1[P ! l]

let P be QC-pred_symbol of k,Al; :: thesis: for l being CQC-variable_list of k,Al holds S1[P ! l]
let l be CQC-variable_list of k,Al; :: thesis: S1[P ! l]
let J2 be interpretation of Al2,A; :: thesis: for Jp being interpretation of Al,A
for v2 being Element of Valuations_in (Al2,A)
for vp being Element of Valuations_in (Al,A) st Jp = J2 | () & vp = v2 | () holds
( J2,v2 |= Al2 -Cast (P ! l) iff Jp,vp |= P ! l )

let Jp be interpretation of Al,A; :: thesis: for v2 being Element of Valuations_in (Al2,A)
for vp being Element of Valuations_in (Al,A) st Jp = J2 | () & vp = v2 | () holds
( J2,v2 |= Al2 -Cast (P ! l) iff Jp,vp |= P ! l )

let v2 be Element of Valuations_in (Al2,A); :: thesis: for vp being Element of Valuations_in (Al,A) st Jp = J2 | () & vp = v2 | () holds
( J2,v2 |= Al2 -Cast (P ! l) iff Jp,vp |= P ! l )

let vp be Element of Valuations_in (Al,A); :: thesis: ( Jp = J2 | () & vp = v2 | () implies ( J2,v2 |= Al2 -Cast (P ! l) iff Jp,vp |= P ! l ) )
assume A3: ( Jp = J2 | () & vp = v2 | () ) ; :: thesis: ( J2,v2 |= Al2 -Cast (P ! l) iff Jp,vp |= P ! l )
set p = P ! l;
the_arity_of P = len l by Th1;
then A4: P ! l = <*P*> ^ l by QC_LANG1:def 12;
( P is QC-pred_symbol of k,Al2 & l is CQC-variable_list of k,Al2 ) by ;
then consider P2 being QC-pred_symbol of k,Al2, l2 being CQC-variable_list of k,Al2 such that
A5: ( P = P2 & l = l2 ) ;
A6: the_arity_of P2 = len l2 by Th1;
A7: v2 *' l2 = vp *' l
proof
A8: bound_QC-variables Al c= bound_QC-variables Al2 by Th4;
A9: for j being Nat st 1 <= j & j <= len l holds
( l . j in bound_QC-variables Al iff l . j in bound_QC-variables Al2 )
proof
let j be Nat; :: thesis: ( 1 <= j & j <= len l implies ( l . j in bound_QC-variables Al iff l . j in bound_QC-variables Al2 ) )
assume A10: ( 1 <= j & j <= len l ) ; :: thesis: ( l . j in bound_QC-variables Al iff l . j in bound_QC-variables Al2 )
thus ( l . j in bound_QC-variables Al implies l . j in bound_QC-variables Al2 ) by A8; :: thesis: ( l . j in bound_QC-variables Al2 implies l . j in bound_QC-variables Al )
end;
set t1 = { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in bound_QC-variables Al ) } ;
set t2 = { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in bound_QC-variables Al2 ) } ;
A11: { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in bound_QC-variables Al ) } = { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in bound_QC-variables Al2 ) }
proof
thus { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in bound_QC-variables Al ) } c= { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in bound_QC-variables Al2 ) } :: according to XBOOLE_0:def 10 :: thesis: { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in bound_QC-variables Al2 ) } c= { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in bound_QC-variables Al ) }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in bound_QC-variables Al ) } or x in { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in bound_QC-variables Al2 ) } )
assume x in { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in bound_QC-variables Al ) } ; :: thesis: x in { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in bound_QC-variables Al2 ) }
then consider i being Nat such that
A12: ( x = l . i & 1 <= i & i <= len l & l . i in bound_QC-variables Al ) ;
( x = l . i & 1 <= i & i <= len l & l . i in bound_QC-variables Al2 ) by ;
hence x in { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in bound_QC-variables Al2 ) } ; :: thesis: verum
end;
thus { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in bound_QC-variables Al2 ) } c= { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in bound_QC-variables Al ) } :: thesis: verum
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in bound_QC-variables Al2 ) } or x in { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in bound_QC-variables Al ) } )
assume x in { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in bound_QC-variables Al2 ) } ; :: thesis: x in { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in bound_QC-variables Al ) }
then consider i being Nat such that
A13: ( x = l . i & 1 <= i & i <= len l & l . i in bound_QC-variables Al2 ) ;
( x = l . i & 1 <= i & i <= len l & l . i in bound_QC-variables Al ) by ;
hence x in { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in bound_QC-variables Al ) } ; :: thesis: verum
end;
end;
A14: still_not-bound_in l = still_not-bound_in l2 by ;
A15: vp | = v2 | () by
.= v2 | by XBOOLE_1:28 ;
v2 *' l2 = l * (vp | ) by
.= vp *' l by SUBLEMMA:59 ;
hence v2 *' l2 = vp *' l ; :: thesis: verum
end;
A16: ( J2,v2 |= Al2 -Cast (P ! l) implies Jp,vp |= P ! l )
proof
assume J2,v2 |= Al2 -Cast (P ! l) ; :: thesis: Jp,vp |= P ! l
then J2,v2 |= P2 ! l2 by ;
then (Valid ((P2 ! l2),J2)) . v2 = TRUE by VALUAT_1:def 7;
then (l2 'in' (J2 . P2)) . v2 = TRUE by VALUAT_1:6;
then A17: vp *' l in J2 . P2 by ;
vp *' l in Jp . P by ;
then (l 'in' (Jp . P)) . vp = TRUE by VALUAT_1:def 4;
then (Valid ((P ! l),Jp)) . vp = TRUE by VALUAT_1:6;
hence Jp,vp |= P ! l by VALUAT_1:def 7; :: thesis: verum
end;
( not J2,v2 |= Al2 -Cast (P ! l) implies not Jp,vp |= P ! l )
proof
assume not J2,v2 |= Al2 -Cast (P ! l) ; :: thesis: not Jp,vp |= P ! l
then not J2,v2 |= P2 ! l2 by ;
then not (Valid ((P2 ! l2),J2)) . v2 = TRUE by VALUAT_1:def 7;
then not (l2 'in' (J2 . P2)) . v2 = TRUE by VALUAT_1:6;
then A18: not vp *' l in J2 . P2 by ;
not vp *' l in Jp . P by ;
then not (l 'in' (Jp . P)) . vp = TRUE by VALUAT_1:def 4;
then not (Valid ((P ! l),Jp)) . vp = TRUE by VALUAT_1:6;
hence not Jp,vp |= P ! l by VALUAT_1:def 7; :: thesis: verum
end;
hence ( J2,v2 |= Al2 -Cast (P ! l) iff Jp,vp |= P ! l ) by A16; :: thesis: verum
end;
A19: for p being Element of CQC-WFF Al st S1[p] holds
S1[ 'not' p]
proof
let p be Element of CQC-WFF Al; :: thesis: ( S1[p] implies S1[ 'not' p] )
assume A20: S1[p] ; :: thesis: S1[ 'not' p]
let J2 be interpretation of Al2,A; :: thesis: for Jp being interpretation of Al,A
for v2 being Element of Valuations_in (Al2,A)
for vp being Element of Valuations_in (Al,A) st Jp = J2 | () & vp = v2 | () holds
( J2,v2 |= Al2 -Cast () iff Jp,vp |= 'not' p )

let Jp be interpretation of Al,A; :: thesis: for v2 being Element of Valuations_in (Al2,A)
for vp being Element of Valuations_in (Al,A) st Jp = J2 | () & vp = v2 | () holds
( J2,v2 |= Al2 -Cast () iff Jp,vp |= 'not' p )

let v2 be Element of Valuations_in (Al2,A); :: thesis: for vp being Element of Valuations_in (Al,A) st Jp = J2 | () & vp = v2 | () holds
( J2,v2 |= Al2 -Cast () iff Jp,vp |= 'not' p )

let vp be Element of Valuations_in (Al,A); :: thesis: ( Jp = J2 | () & vp = v2 | () implies ( J2,v2 |= Al2 -Cast () iff Jp,vp |= 'not' p ) )
assume A21: ( Jp = J2 | () & vp = v2 | () ) ; :: thesis: ( J2,v2 |= Al2 -Cast () iff Jp,vp |= 'not' p )
per cases ( not J2,v2 |= Al2 -Cast p or J2,v2 |= Al2 -Cast p ) ;
suppose A22: not J2,v2 |= Al2 -Cast p ; :: thesis: ( J2,v2 |= Al2 -Cast () iff Jp,vp |= 'not' p )
then A23: not Jp,vp |= p by ;
J2,v2 |= 'not' (Al2 -Cast p) by ;
hence ( J2,v2 |= Al2 -Cast () iff Jp,vp |= 'not' p ) by ; :: thesis: verum
end;
suppose A24: J2,v2 |= Al2 -Cast p ; :: thesis: ( J2,v2 |= Al2 -Cast () iff Jp,vp |= 'not' p )
then A25: Jp,vp |= p by ;
not J2,v2 |= 'not' (Al2 -Cast p) by ;
hence ( J2,v2 |= Al2 -Cast () iff Jp,vp |= 'not' p ) by ; :: thesis: verum
end;
end;
end;
A26: for p, r being Element of CQC-WFF Al st S1[p] & S1[r] holds
S1[p '&' r]
proof
let p, r be Element of CQC-WFF Al; :: thesis: ( S1[p] & S1[r] implies S1[p '&' r] )
assume A27: ( S1[p] & S1[r] ) ; :: thesis: S1[p '&' r]
let J2 be interpretation of Al2,A; :: thesis: for Jp being interpretation of Al,A
for v2 being Element of Valuations_in (Al2,A)
for vp being Element of Valuations_in (Al,A) st Jp = J2 | () & vp = v2 | () holds
( J2,v2 |= Al2 -Cast (p '&' r) iff Jp,vp |= p '&' r )

let Jp be interpretation of Al,A; :: thesis: for v2 being Element of Valuations_in (Al2,A)
for vp being Element of Valuations_in (Al,A) st Jp = J2 | () & vp = v2 | () holds
( J2,v2 |= Al2 -Cast (p '&' r) iff Jp,vp |= p '&' r )

let v2 be Element of Valuations_in (Al2,A); :: thesis: for vp being Element of Valuations_in (Al,A) st Jp = J2 | () & vp = v2 | () holds
( J2,v2 |= Al2 -Cast (p '&' r) iff Jp,vp |= p '&' r )

let vp be Element of Valuations_in (Al,A); :: thesis: ( Jp = J2 | () & vp = v2 | () implies ( J2,v2 |= Al2 -Cast (p '&' r) iff Jp,vp |= p '&' r ) )
assume A28: ( Jp = J2 | () & vp = v2 | () ) ; :: thesis: ( J2,v2 |= Al2 -Cast (p '&' r) iff Jp,vp |= p '&' r )
A29: ( J2,v2 |= Al2 -Cast (p '&' r) implies Jp,vp |= p '&' r )
proof
assume J2,v2 |= Al2 -Cast (p '&' r) ; :: thesis: Jp,vp |= p '&' r
then J2,v2 |= (Al2 -Cast p) '&' (Al2 -Cast r) ;
then ( J2,v2 |= Al2 -Cast p & J2,v2 |= Al2 -Cast r ) by VALUAT_1:18;
then ( Jp,vp |= p & Jp,vp |= r ) by ;
hence Jp,vp |= p '&' r by VALUAT_1:18; :: thesis: verum
end;
( Jp,vp |= p '&' r implies J2,v2 |= Al2 -Cast (p '&' r) )
proof
assume Jp,vp |= p '&' r ; :: thesis: J2,v2 |= Al2 -Cast (p '&' r)
then ( Jp,vp |= p & Jp,vp |= r ) by VALUAT_1:18;
then ( J2,v2 |= Al2 -Cast p & J2,v2 |= Al2 -Cast r ) by ;
then J2,v2 |= (Al2 -Cast p) '&' (Al2 -Cast r) by VALUAT_1:18;
hence J2,v2 |= Al2 -Cast (p '&' r) ; :: thesis: verum
end;
hence ( J2,v2 |= Al2 -Cast (p '&' r) iff Jp,vp |= p '&' r ) by A29; :: thesis: verum
end;
A30: for x being bound_QC-variable of Al
for r being Element of CQC-WFF Al st S1[r] holds
S1[ All (x,r)]
proof
let x be bound_QC-variable of Al; :: thesis: for r being Element of CQC-WFF Al st S1[r] holds
S1[ All (x,r)]

let r be Element of CQC-WFF Al; :: thesis: ( S1[r] implies S1[ All (x,r)] )
assume A31: S1[r] ; :: thesis: S1[ All (x,r)]
let J2 be interpretation of Al2,A; :: thesis: for Jp being interpretation of Al,A
for v2 being Element of Valuations_in (Al2,A)
for vp being Element of Valuations_in (Al,A) st Jp = J2 | () & vp = v2 | () holds
( J2,v2 |= Al2 -Cast (All (x,r)) iff Jp,vp |= All (x,r) )

let Jp be interpretation of Al,A; :: thesis: for v2 being Element of Valuations_in (Al2,A)
for vp being Element of Valuations_in (Al,A) st Jp = J2 | () & vp = v2 | () holds
( J2,v2 |= Al2 -Cast (All (x,r)) iff Jp,vp |= All (x,r) )

let v2 be Element of Valuations_in (Al2,A); :: thesis: for vp being Element of Valuations_in (Al,A) st Jp = J2 | () & vp = v2 | () holds
( J2,v2 |= Al2 -Cast (All (x,r)) iff Jp,vp |= All (x,r) )

let vp be Element of Valuations_in (Al,A); :: thesis: ( Jp = J2 | () & vp = v2 | () implies ( J2,v2 |= Al2 -Cast (All (x,r)) iff Jp,vp |= All (x,r) ) )
assume A32: ( Jp = J2 | () & vp = v2 | () ) ; :: thesis: ( J2,v2 |= Al2 -Cast (All (x,r)) iff Jp,vp |= All (x,r) )
A33: ( J2,v2 |= Al2 -Cast (All (x,r)) implies Jp,vp |= All (x,r) )
proof
assume J2,v2 |= Al2 -Cast (All (x,r)) ; :: thesis: Jp,vp |= All (x,r)
then A34: J2,v2 |= All ((Al2 -Cast x),(Al2 -Cast r)) ;
for vp1 being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
vp1 . y = vp . y ) holds
Jp,vp1 |= r
proof
let vp1 be Element of Valuations_in (Al,A); :: thesis: ( ( for y being bound_QC-variable of Al st x <> y holds
vp1 . y = vp . y ) implies Jp,vp1 |= r )

assume A35: for y being bound_QC-variable of Al st x <> y holds
vp1 . y = vp . y ; :: thesis: Jp,vp1 |= r
set s = (Al2 -Cast x) .--> (vp1 . x);
A36: (Al2 -Cast x) .--> (vp1 . x) = {(Al2 -Cast x)} --> (vp1 . x) by FUNCOP_1:def 9;
set v21 = v2 +* ((Al2 -Cast x) .--> (vp1 . x));
v2 is Element of Funcs ((),A) by VALUAT_1:def 1;
then A37: ( dom v2 = bound_QC-variables Al2 & rng v2 c= A ) by FUNCT_2:92;
dom ((Al2 -Cast x) .--> (vp1 . x)) = {(Al2 -Cast x)} by A36;
then dom (v2 +* ((Al2 -Cast x) .--> (vp1 . x))) = (dom v2) \/ {(Al2 -Cast x)} by FUNCT_4:def 1;
then A38: dom (v2 +* ((Al2 -Cast x) .--> (vp1 . x))) = bound_QC-variables Al2 by ;
A39: (rng v2) \/ {(vp1 . x)} c= A by ;
rng ((Al2 -Cast x) .--> (vp1 . x)) = {(vp1 . x)} by ;
then rng (v2 +* ((Al2 -Cast x) .--> (vp1 . x))) c= (rng v2) \/ {(vp1 . x)} by FUNCT_4:17;
then rng (v2 +* ((Al2 -Cast x) .--> (vp1 . x))) c= A by A39;
then v2 +* ((Al2 -Cast x) .--> (vp1 . x)) is Element of Funcs ((),A) by ;
then reconsider v21 = v2 +* ((Al2 -Cast x) .--> (vp1 . x)) as Element of Valuations_in (Al2,A) by VALUAT_1:def 1;
for y being bound_QC-variable of Al2 st Al2 -Cast x <> y holds
v21 . y = v2 . y by FUNCT_4:83;
then A40: J2,v21 |= Al2 -Cast r by ;
vp1 is Element of Funcs ((),A) by VALUAT_1:def 1;
then A41: dom vp1 = bound_QC-variables Al by FUNCT_2:92
.= (dom v21) /\ () by ;
for c being object st c in dom vp1 holds
vp1 . c = v21 . c
proof
let c be object ; :: thesis: ( c in dom vp1 implies vp1 . c = v21 . c )
assume A42: c in dom vp1 ; :: thesis: vp1 . c = v21 . c
per cases ( c = Al2 -Cast x or c <> Al2 -Cast x ) ;
suppose A43: c = Al2 -Cast x ; :: thesis: vp1 . c = v21 . c
then c in dom ((Al2 -Cast x) .--> (vp1 . x)) by FUNCOP_1:74;
hence v21 . c = ((Al2 -Cast x) .--> (vp1 . x)) . c by FUNCT_4:13
.= vp1 . c by ;
:: thesis: verum
end;
suppose A44: c <> Al2 -Cast x ; :: thesis: vp1 . c = v21 . c
reconsider c = c as bound_QC-variable of Al by ;
v21 . c = v2 . c by
.= (v2 | ()) . c by FUNCT_1:49
.= vp1 . c by ;
hence vp1 . c = v21 . c ; :: thesis: verum
end;
end;
end;
then v21 | () = vp1 by ;
hence Jp,vp1 |= r by ; :: thesis: verum
end;
hence Jp,vp |= All (x,r) by VALUAT_1:29; :: thesis: verum
end;
( Jp,vp |= All (x,r) implies J2,v2 |= Al2 -Cast (All (x,r)) )
proof
assume A45: Jp,vp |= All (x,r) ; :: thesis: J2,v2 |= Al2 -Cast (All (x,r))
for v21 being Element of Valuations_in (Al2,A) st ( for y being bound_QC-variable of Al2 st Al2 -Cast x <> y holds
v21 . y = v2 . y ) holds
J2,v21 |= Al2 -Cast r
proof
let v21 be Element of Valuations_in (Al2,A); :: thesis: ( ( for y being bound_QC-variable of Al2 st Al2 -Cast x <> y holds
v21 . y = v2 . y ) implies J2,v21 |= Al2 -Cast r )

assume A46: for y being bound_QC-variable of Al2 st Al2 -Cast x <> y holds
v21 . y = v2 . y ; :: thesis: J2,v21 |= Al2 -Cast r
set s = x .--> (v21 . (Al2 -Cast x));
A47: x .--> (v21 . (Al2 -Cast x)) = {x} --> (v21 . (Al2 -Cast x)) by FUNCOP_1:def 9;
set vp1 = vp +* (x .--> (v21 . (Al2 -Cast x)));
vp is Element of Funcs ((),A) by VALUAT_1:def 1;
then A48: ( dom vp = bound_QC-variables Al & rng vp c= A ) by FUNCT_2:92;
dom (x .--> (v21 . (Al2 -Cast x))) = {x} by A47;
then dom (vp +* (x .--> (v21 . (Al2 -Cast x)))) = (dom vp) \/ {x} by FUNCT_4:def 1;
then A49: dom (vp +* (x .--> (v21 . (Al2 -Cast x)))) = bound_QC-variables Al by ;
A50: (rng vp) \/ {(v21 . (Al2 -Cast x))} c= A by ;
rng (x .--> (v21 . (Al2 -Cast x))) = {(v21 . (Al2 -Cast x))} by ;
then rng (vp +* (x .--> (v21 . (Al2 -Cast x)))) c= (rng vp) \/ {(v21 . (Al2 -Cast x))} by FUNCT_4:17;
then rng (vp +* (x .--> (v21 . (Al2 -Cast x)))) c= A by A50;
then vp +* (x .--> (v21 . (Al2 -Cast x))) is Element of Funcs ((),A) by ;
then reconsider vp1 = vp +* (x .--> (v21 . (Al2 -Cast x))) as Element of Valuations_in (Al,A) by VALUAT_1:def 1;
for y being bound_QC-variable of Al st x <> y holds
vp1 . y = vp . y by FUNCT_4:83;
then A51: Jp,vp1 |= r by ;
v21 is Element of Funcs ((),A) by VALUAT_1:def 1;
then A52: dom v21 = bound_QC-variables Al2 by FUNCT_2:92;
vp1 is Element of Funcs ((),A) by VALUAT_1:def 1;
then A53: dom vp1 = bound_QC-variables Al by FUNCT_2:92
.= (dom v21) /\ () by ;
for c being object st c in dom vp1 holds
vp1 . c = v21 . c
proof
let c be object ; :: thesis: ( c in dom vp1 implies vp1 . c = v21 . c )
assume A54: c in dom vp1 ; :: thesis: vp1 . c = v21 . c
per cases ( c = x or c <> x ) ;
suppose A55: c = x ; :: thesis: vp1 . c = v21 . c
then c in dom (x .--> (v21 . (Al2 -Cast x))) by FUNCOP_1:74;
then vp1 . c = (x .--> (v21 . (Al2 -Cast x))) . x by
.= v21 . c by ;
hence vp1 . c = v21 . c ; :: thesis: verum
end;
suppose A56: c <> x ; :: thesis: vp1 . c = v21 . c
A57: c in bound_QC-variables Al by ;
vp1 is Element of Funcs ((),A) by VALUAT_1:def 1;
then dom vp1 = bound_QC-variables Al by FUNCT_2:92;
then A58: dom vp1 c= bound_QC-variables Al2 by Th4;
vp1 . c = vp . c by
.= v2 . c by
.= v21 . c by A56, A46, A54, A58 ;
hence vp1 . c = v21 . c ; :: thesis: verum
end;
end;
end;
then v21 | () = vp1 by ;
hence J2,v21 |= Al2 -Cast r by ; :: thesis: verum
end;
then J2,v2 |= All ((Al2 -Cast x),(Al2 -Cast r)) by VALUAT_1:29;
hence J2,v2 |= Al2 -Cast (All (x,r)) ; :: thesis: verum
end;
hence ( J2,v2 |= Al2 -Cast (All (x,r)) iff Jp,vp |= All (x,r) ) by A33; :: thesis: verum
end;
A59: for r, s being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for k being Nat
for l being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( S1[ VERUM Al] & S1[P ! l] & ( S1[r] implies S1[ 'not' r] ) & ( S1[r] & S1[s] implies S1[r '&' s] ) & ( S1[r] implies S1[ All (x,r)] ) ) by A1, A2, A19, A26, A30;
for r being Element of CQC-WFF Al holds S1[r] from hence ( Jp = J2 | () & vp = v2 | () implies ( J2,v2 |= Al2 -Cast r iff Jp,vp |= r ) ) ; :: thesis: verum