let p be Element of CQC-WFF ; :: thesis: for x being bound_QC-variable st ( for Sub being CQC_Substitution ex S being Element of CQC-Sub-WFF st
( S `1 = p & S `2 = Sub ) ) holds
for Sub being CQC_Substitution ex S being Element of CQC-Sub-WFF st
( S `1 = All x,p & S `2 = Sub )
let x be bound_QC-variable; :: thesis: ( ( for Sub being CQC_Substitution ex S being Element of CQC-Sub-WFF st
( S `1 = p & S `2 = Sub ) ) implies for Sub being CQC_Substitution ex S being Element of CQC-Sub-WFF st
( S `1 = All x,p & S `2 = Sub ) )
assume A1: for Sub being CQC_Substitution ex S being Element of CQC-Sub-WFF st
( S `1 = p & S `2 = Sub ) ; :: thesis: for Sub being CQC_Substitution ex S being Element of CQC-Sub-WFF st
( S `1 = All x,p & S `2 = Sub )
let Sub be CQC_Substitution; :: thesis: ex S being Element of CQC-Sub-WFF st
( S `1 = All x,p & S `2 = Sub )
set Sub1 = (@ (RestrictSub x,(All x,p),Sub)) +* (x | (S_Bound [(All x,p),Sub]));
reconsider Sub1 = (@ (RestrictSub x,(All x,p),Sub)) +* (x | (S_Bound [(All x,p),Sub])) as CQC_Substitution by PARTFUN1:119, SUBSTUT1:def 1;
consider S being Element of CQC-Sub-WFF such that
A2: ( S `1 = p & S `2 = Sub1 ) by A1;
consider S1 being Element of CQC-Sub-WFF such that
A3: S1 = [(All x,p),Sub] by A2, Th10;
take S1 ; :: thesis: ( S1 `1 = All x,p & S1 `2 = Sub )
thus ( S1 `1 = All x,p & S1 `2 = Sub ) by A3, MCART_1:7; :: thesis: verum