defpred S₁[ set , set ] means ex P9 being Element of QC-pred_symbols st
( P9 = $1 & $2 = { ll where ll is CQC-variable_list of the_arity_of P9 : CX |- P9 ! ll } );
set A = QC-pred_symbols ;
A1: for a being set st a in QC-pred_symbols holds
ex b being set st S₁[a,b]

proof

let a be set ; :: thesis: ( a in QC-pred_symbols implies ex b being set st S₁[a,b] )
assume a in QC-pred_symbols ; :: thesis: ex b being set st S₁[a,b]
then reconsider a = a as Element of QC-pred_symbols ;
consider b being set such that
A2: b = { ll where ll is CQC-variable_list of the_arity_of a : CX |- a ! ll } ;
take b ; :: thesis: S₁[a,b]
take a ; :: thesis: ( a = a & b = { ll where ll is CQC-variable_list of the_arity_of a : CX |- a ! ll } )
thus ( a = a & b = { ll where ll is CQC-variable_list of the_arity_of a : CX |- a ! ll } ) by A2; :: thesis: verum

end;

consider f being Function such that
A3: ( dom f = QC-pred_symbols & ( for a being set st a in QC-pred_symbols holds
S₁[a,f . a] ) ) from CLASSES1:sch 1(A1);
A4: for P being Element of QC-pred_symbols
for r being Element of relations_on HCar st f . P = r holds
for a being set holds
( a in r iff ex ll being CQC-variable_list of the_arity_of P st
( a = ll & CX |- P ! ll ) )

proof

let P be Element of QC-pred_symbols ; :: thesis: for r being Element of relations_on HCar st f . P = r holds
for a being set holds
( a in r iff ex ll being CQC-variable_list of the_arity_of P st
( a = ll & CX |- P ! ll ) )
let r be Element of relations_on HCar; :: thesis: ( f . P = r implies for a being set holds
( a in r iff ex ll being CQC-variable_list of the_arity_of P st
( a = ll & CX |- P ! ll ) ) )
assume A5: f . P = r ; :: thesis: for a being set holds
( a in r iff ex ll being CQC-variable_list of the_arity_of P st
( a = ll & CX |- P ! ll ) )
let a be set ; :: thesis: ( a in r iff ex ll being CQC-variable_list of the_arity_of P st
( a = ll & CX |- P ! ll ) )
thus ( a in r implies ex ll being CQC-variable_list of the_arity_of P st
( a = ll & CX |- P ! ll ) ) :: thesis: ( ex ll being CQC-variable_list of the_arity_of P st
( a = ll & CX |- P ! ll ) implies a in r )

proof

assume A6: a in r ; :: thesis: ex ll being CQC-variable_list of the_arity_of P st
( a = ll & CX |- P ! ll )
ex P9 being Element of QC-pred_symbols st
( P9 = P & f . P = { ll where ll is CQC-variable_list of the_arity_of P9 : CX |- P9 ! ll } ) by A3;
hence ex ll being CQC-variable_list of the_arity_of P st
( a = ll & CX |- P ! ll ) by A5, A6; :: thesis: verum

end;

thus ( ex ll being CQC-variable_list of the_arity_of P st
( a = ll & CX |- P ! ll ) implies a in r ) :: thesis: verum

proof

given ll being CQC-variable_list of the_arity_of P such that A7: ( a = ll & CX |- P ! ll ) ; :: thesis: a in r
ex P9 being Element of QC-pred_symbols st
( P9 = P & f . P = { l where l is CQC-variable_list of the_arity_of P9 : CX |- P9 ! l } ) by A3;
hence a in r by A5, A7; :: thesis: verum

end;

end;

A8: for P being Element of QC-pred_symbols
for r being Element of relations_on HCar holds
( not f . P = r or r = empty_rel HCar or the_arity_of P = the_arity_of r )

proof

let P be Element of QC-pred_symbols ; :: thesis: for r being Element of relations_on HCar holds
( not f . P = r or r = empty_rel HCar or the_arity_of P = the_arity_of r )
let r be Element of relations_on HCar; :: thesis: ( not f . P = r or r = empty_rel HCar or the_arity_of P = the_arity_of r )
assume A9: f . P = r ; :: thesis: ( r = empty_rel HCar or the_arity_of P = the_arity_of r )
consider P9 being Element of QC-pred_symbols such that
A10: ( P9 = P & f . P = { ll where ll is CQC-variable_list of the_arity_of P9 : CX |- P9 ! ll } ) by A3;
assume A11: not r = empty_rel HCar ; :: thesis: the_arity_of P = the_arity_of r
then r <> {} by MARGREL1:9;
then consider a being set such that
A12: a in r by XBOOLE_0:def 1;
consider ll9 being CQC-variable_list of the_arity_of P9 such that
A13: a = ll9 and
CX |- P9 ! ll9 by A9, A12, A10;
rng ll9 c= bound_QC-variables by RELAT_1:def 19;
then reconsider a = a as FinSequence of HCar by A13, FINSEQ_1:def 4;
the_arity_of r = len a by A11, A12, MARGREL1:def 10;
hence the_arity_of P = the_arity_of r by A10, A13, CARD_1:def 7; :: thesis: verum

end;

for b being set st b in rng f holds
b in relations_on HCar

proof

let b be set ; :: thesis: ( b in rng f implies b in relations_on HCar )
assume b in rng f ; :: thesis: b in relations_on HCar
then consider a being set such that
A14: a in dom f and
A15: b = f . a by FUNCT_1:def 3;
consider P9 being Element of QC-pred_symbols such that
A16: ( P9 = a & f . a = { ll where ll is CQC-variable_list of the_arity_of P9 : CX |- P9 ! ll } ) by A3, A14;
for c being set st c in b holds
c in HCar *

proof

let c be set ; :: thesis: ( c in b implies c in HCar * )
assume c in b ; :: thesis: c in HCar *
then consider ll being CQC-variable_list of the_arity_of P9 such that
A17: c = ll and
CX |- P9 ! ll by A15, A16;
rng ll c= bound_QC-variables by RELAT_1:def 19;
then ll is FinSequence of HCar by FINSEQ_1:def 4;
hence c in HCar * by A17, FINSEQ_1:def 11; :: thesis: verum

end;

then A18: b c= HCar * by TARSKI:def 3;
for fin, fin9 being FinSequence of HCar st fin in b & fin9 in b holds
len fin = len fin9

proof

let fin, fin9 be FinSequence of HCar ; :: thesis: ( fin in b & fin9 in b implies len fin = len fin9 )
assume that
A19: fin in b and
A20: fin9 in b ; :: thesis: len fin = len fin9
ex ll being CQC-variable_list of the_arity_of P9 st
( fin = ll & CX |- P9 ! ll ) by A15, A16, A19;
then A21: len fin = the_arity_of P9 by CARD_1:def 7;
ex ll9 being CQC-variable_list of the_arity_of P9 st
( fin9 = ll9 & CX |- P9 ! ll9 ) by A15, A16, A20;
hence len fin = len fin9 by A21, CARD_1:def 7; :: thesis: verum

end;

hence b in relations_on HCar by A18, MARGREL1:def 7; :: thesis: verum

end;

then rng f c= relations_on HCar by TARSKI:def 3;
then reconsider f = f as Function of QC-pred_symbols,(relations_on HCar) by A3, FUNCT_2:2;
reconsider f = f as interpretation of HCar by A8, VALUAT_1:def 5;
take f ; :: thesis: for P being Element of QC-pred_symbols
for r being Element of relations_on HCar st f . P = r holds
for a being set holds
( a in r iff ex ll being CQC-variable_list of the_arity_of P st
( a = ll & CX |- P ! ll ) )
thus for P being Element of QC-pred_symbols
for r being Element of relations_on HCar st f . P = r holds
for a being set holds
( a in r iff ex ll being CQC-variable_list of the_arity_of P st
( a = ll & CX |- P ! ll ) ) by A4; :: thesis: verum