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

proof

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

end;

consider f being Function such that
A3: ( dom f = QC-pred_symbols Al & ( for a being object st a in QC-pred_symbols Al holds
S₁[a,f . a] ) ) from CLASSES1:sch 1(A1);
A4: for P being Element of QC-pred_symbols Al
for r being Element of relations_on (HCar Al) 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,Al st
( a = ll & CX |- P ! ll ) )

proof

let P be Element of QC-pred_symbols Al; :: thesis: for r being Element of relations_on (HCar Al) 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,Al st
( a = ll & CX |- P ! ll ) )
let r be Element of relations_on (HCar Al); :: 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,Al 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,Al 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,Al st
( a = ll & CX |- P ! ll ) )
thus ( a in r implies ex ll being CQC-variable_list of the_arity_of P,Al st
( a = ll & CX |- P ! ll ) ) :: thesis: ( ex ll being CQC-variable_list of the_arity_of P,Al 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,Al st
( a = ll & CX |- P ! ll )
ex P9 being Element of QC-pred_symbols Al st
( P9 = P & f . P = { ll where ll is CQC-variable_list of the_arity_of P9,Al : CX |- P9 ! ll } ) by A3;
hence ex ll being CQC-variable_list of the_arity_of P,Al st
( a = ll & CX |- P ! ll ) by A5, A6; :: thesis: verum

end;

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

proof

given ll being CQC-variable_list of the_arity_of P,Al such that A7: ( a = ll & CX |- P ! ll ) ; :: thesis: a in r
ex P9 being Element of QC-pred_symbols Al st
( P9 = P & f . P = { l where l is CQC-variable_list of the_arity_of P9,Al : 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 Al
for r being Element of relations_on (HCar Al) holds
( not f . P = r or r = empty_rel (HCar Al) or the_arity_of P = the_arity_of r )

proof

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

proof

let b be object ; :: thesis: ( b in rng f implies b in relations_on (HCar Al) )
reconsider bb = b as set by TARSKI:1;
assume b in rng f ; :: thesis: b in relations_on (HCar Al)
then consider a being object 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 Al such that
A16: ( P9 = a & f . a = { ll where ll is CQC-variable_list of the_arity_of P9,Al : CX |- P9 ! ll } ) by A3, A14;
for c being object st c in bb holds
c in (HCar Al) *

proof

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

end;

then A18: bb c= (HCar Al) * ;
for fin, fin9 being FinSequence of HCar Al st fin in bb & fin9 in bb holds
len fin = len fin9

proof

let fin, fin9 be FinSequence of HCar Al; :: thesis: ( fin in bb & fin9 in bb implies len fin = len fin9 )
assume that
A19: fin in bb and
A20: fin9 in bb ; :: thesis: len fin = len fin9
ex ll being CQC-variable_list of the_arity_of P9,Al 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,Al 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 Al) by A18, MARGREL1:def 7; :: thesis: verum

end;

then rng f c= relations_on (HCar Al) ;
then reconsider f = f as Function of (QC-pred_symbols Al),(relations_on (HCar Al)) by A3, FUNCT_2:2;
reconsider f = f as interpretation of Al, HCar Al by A8, VALUAT_1:def 5;
take f ; :: thesis: for P being Element of QC-pred_symbols Al
for r being Element of relations_on (HCar Al) 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,Al st
( a = ll & CX |- P ! ll ) )
thus for P being Element of QC-pred_symbols Al
for r being Element of relations_on (HCar Al) 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,Al st
( a = ll & CX |- P ! ll ) ) by A4; :: thesis: verum