defpred S_{1}[ 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_{1}[a,b]

A3: ( dom f = QC-pred_symbols Al & ( for a being object st a in QC-pred_symbols Al holds

S_{1}[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 ) )

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 )

b in 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

( 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

proof

consider f being Function such that
let a be object ; :: thesis: ( a in QC-pred_symbols Al implies ex b being object st S_{1}[a,b] )

assume a in QC-pred_symbols Al ; :: thesis: ex b being object st S_{1}[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_{1}[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;assume a in QC-pred_symbols Al ; :: thesis: ex b being object st S

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

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

A3: ( dom f = QC-pred_symbols Al & ( for a being object st a in QC-pred_symbols Al holds

S

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

A8:
for P being Element of QC-pred_symbols Al
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 )

( a = ll & CX |- P ! ll ) implies a in r ) :: thesis: verum

end;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

thus
( ex ll being CQC-variable_list of the_arity_of P,Al st
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;( 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

( 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;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

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

for b being object st b in rng f holds
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;( 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

b in relations_on (HCar Al)

proof

then
rng f c= relations_on (HCar Al)
;
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) *

for fin, fin9 being FinSequence of HCar Al st fin in bb & fin9 in bb holds

len fin = len fin9

end;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

then A18:
bb c= (HCar Al) *
;
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;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

for fin, fin9 being FinSequence of HCar Al st fin in bb & fin9 in bb holds

len fin = len fin9

proof

hence
b in relations_on (HCar Al)
by A18, MARGREL1:def 7; :: thesis: verum
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;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

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