:: PRALG_2 semantic presentation
begin
registration
let X be functional non empty with_common_domain set ;
cluster -> DOM X -defined for Element of X;
coherence
for b1 being Element of X holds b1 is DOM X -defined
proof
let x be Element of X; ::_thesis: x is DOM X -defined
DOM X = dom x by CARD_3:108;
hence x is DOM X -defined by RELAT_1:def_18; ::_thesis: verum
end;
end;
registration
let X be functional non empty with_common_domain set ;
cluster -> total for Element of X;
coherence
for b1 being Element of X holds b1 is total
proof
let x be Element of X; ::_thesis: x is total
DOM X = dom x by CARD_3:108;
hence x is total by PARTFUN1:def_2; ::_thesis: verum
end;
end;
begin
definition
let F be Function;
func Commute F -> Function means :Def1: :: PRALG_2:def 1
( ( for x being set holds
( x in dom it iff ex f being Function st
( f in dom F & x = commute f ) ) ) & ( for f being Function st f in dom it holds
it . f = F . (commute f) ) );
existence
ex b1 being Function st
( ( for x being set holds
( x in dom b1 iff ex f being Function st
( f in dom F & x = commute f ) ) ) & ( for f being Function st f in dom b1 holds
b1 . f = F . (commute f) ) )
proof
defpred S1[ set , set ] means ex f being Function st
( $1 = f & $2 = commute f );
A1: for x, y1, y2 being set st S1[x,y1] & S1[x,y2] holds
y1 = y2 ;
consider X being set such that
A2: for x being set holds
( x in X iff ex y being set st
( y in dom F & S1[y,x] ) ) from TARSKI:sch_1(A1);
defpred S2[ set , set ] means for f being Function st $1 = f holds
$2 = F . (commute f);
A3: now__::_thesis:_for_x_being_set_st_x_in_X_holds_
ex_y_being_set_st_S2[x,y]
let x be set ; ::_thesis: ( x in X implies ex y being set st S2[x,y] )
assume x in X ; ::_thesis: ex y being set st S2[x,y]
then ex y being set st
( y in dom F & ex f being Function st
( y = f & x = commute f ) ) by A2;
then reconsider f = x as Function ;
take y = F . (commute f); ::_thesis: S2[x,y]
thus S2[x,y] ; ::_thesis: verum
end;
consider G being Function such that
A4: dom G = X and
A5: for x being set st x in X holds
S2[x,G . x] from CLASSES1:sch_1(A3);
take G ; ::_thesis: ( ( for x being set holds
( x in dom G iff ex f being Function st
( f in dom F & x = commute f ) ) ) & ( for f being Function st f in dom G holds
G . f = F . (commute f) ) )
hereby ::_thesis: for f being Function st f in dom G holds
G . f = F . (commute f)
let x be set ; ::_thesis: ( ( x in dom G implies ex f being Function st
( f in dom F & x = commute f ) ) & ( ex f being Function st
( f in dom F & x = commute f ) implies x in dom G ) )
hereby ::_thesis: ( ex f being Function st
( f in dom F & x = commute f ) implies x in dom G )
assume x in dom G ; ::_thesis: ex f being Function st
( f in dom F & x = commute f )
then consider y being set such that
A6: y in dom F and
A7: ex f being Function st
( y = f & x = commute f ) by A2, A4;
reconsider f = y as Function by A7;
take f = f; ::_thesis: ( f in dom F & x = commute f )
thus ( f in dom F & x = commute f ) by A6, A7; ::_thesis: verum
end;
thus ( ex f being Function st
( f in dom F & x = commute f ) implies x in dom G ) by A2, A4; ::_thesis: verum
end;
thus for f being Function st f in dom G holds
G . f = F . (commute f) by A4, A5; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function st ( for x being set holds
( x in dom b1 iff ex f being Function st
( f in dom F & x = commute f ) ) ) & ( for f being Function st f in dom b1 holds
b1 . f = F . (commute f) ) & ( for x being set holds
( x in dom b2 iff ex f being Function st
( f in dom F & x = commute f ) ) ) & ( for f being Function st f in dom b2 holds
b2 . f = F . (commute f) ) holds
b1 = b2
proof
let m, n be Function; ::_thesis: ( ( for x being set holds
( x in dom m iff ex f being Function st
( f in dom F & x = commute f ) ) ) & ( for f being Function st f in dom m holds
m . f = F . (commute f) ) & ( for x being set holds
( x in dom n iff ex f being Function st
( f in dom F & x = commute f ) ) ) & ( for f being Function st f in dom n holds
n . f = F . (commute f) ) implies m = n )
assume that
A8: for x being set holds
( x in dom m iff ex f being Function st
( f in dom F & x = commute f ) ) and
A9: for f being Function st f in dom m holds
m . f = F . (commute f) and
A10: for x being set holds
( x in dom n iff ex f being Function st
( f in dom F & x = commute f ) ) and
A11: for f being Function st f in dom n holds
n . f = F . (commute f) ; ::_thesis: m = n
now__::_thesis:_for_x_being_set_holds_
(_x_in_dom_m_iff_x_in_dom_n_)
let x be set ; ::_thesis: ( x in dom m iff x in dom n )
( x in dom m iff ex f being Function st
( f in dom F & x = commute f ) ) by A8;
hence ( x in dom m iff x in dom n ) by A10; ::_thesis: verum
end;
then A12: dom m = dom n by TARSKI:1;
now__::_thesis:_for_x_being_set_st_x_in_dom_m_holds_
m_._x_=_n_._x
let x be set ; ::_thesis: ( x in dom m implies m . x = n . x )
assume A13: x in dom m ; ::_thesis: m . x = n . x
then consider g being Function such that
g in dom F and
A14: x = commute g by A10, A12;
thus m . x = F . (commute (commute g)) by A9, A13, A14
.= n . x by A11, A12, A13, A14 ; ::_thesis: verum
end;
hence m = n by A12, FUNCT_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def1 defines Commute PRALG_2:def_1_:_
for F, b2 being Function holds
( b2 = Commute F iff ( ( for x being set holds
( x in dom b2 iff ex f being Function st
( f in dom F & x = commute f ) ) ) & ( for f being Function st f in dom b2 holds
b2 . f = F . (commute f) ) ) );
theorem :: PRALG_2:1
for F being Function st dom F = {{}} holds
Commute F = F
proof
let F be Function; ::_thesis: ( dom F = {{}} implies Commute F = F )
assume A1: dom F = {{}} ; ::_thesis: Commute F = F
A2: dom (Commute F) = {{}}
proof
thus dom (Commute F) c= {{}} :: according to XBOOLE_0:def_10 ::_thesis: {{}} c= dom (Commute F)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom (Commute F) or x in {{}} )
assume x in dom (Commute F) ; ::_thesis: x in {{}}
then ex f being Function st
( f in dom F & x = commute f ) by Def1;
then x = {} by A1, FUNCT_6:58, TARSKI:def_1;
hence x in {{}} by TARSKI:def_1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {{}} or x in dom (Commute F) )
assume x in {{}} ; ::_thesis: x in dom (Commute F)
then A3: x = {} by TARSKI:def_1;
{} in dom F by A1, TARSKI:def_1;
hence x in dom (Commute F) by A3, Def1, FUNCT_6:58; ::_thesis: verum
end;
for x being set st x in {{}} holds
(Commute F) . x = F . x
proof
let x be set ; ::_thesis: ( x in {{}} implies (Commute F) . x = F . x )
assume A4: x in {{}} ; ::_thesis: (Commute F) . x = F . x
then x = {} by TARSKI:def_1;
hence (Commute F) . x = F . x by A2, A4, Def1, FUNCT_6:58; ::_thesis: verum
end;
hence Commute F = F by A1, A2, FUNCT_1:2; ::_thesis: verum
end;
definition
let f be Function-yielding Function;
:: original: Frege
redefine func Frege f -> ManySortedFunction of product (doms f) means :Def2: :: PRALG_2:def 2
for g being Function st g in product (doms f) holds
it . g = f .. g;
coherence
Frege f is ManySortedFunction of product (doms f)
proof
A1: dom (Frege f) = product (doms f) by FUNCT_6:def_7;
Frege f is Function-yielding
proof
let x be set ; :: according to FUNCOP_1:def_6 ::_thesis: ( not x in dom (Frege f) or (Frege f) . x is set )
assume A2: x in dom (Frege f) ; ::_thesis: (Frege f) . x is set
then reconsider g = x as Function by A1;
ex h being Function st
( (Frege f) . g = h & dom h = f " (SubFuncs (rng f)) & ( for x being set st x in dom h holds
h . x = (uncurry f) . (x,(g . x)) ) ) by A1, A2, FUNCT_6:def_7;
hence (Frege f) . x is set ; ::_thesis: verum
end;
hence Frege f is ManySortedFunction of product (doms f) by A1, PARTFUN1:def_2, RELAT_1:def_18; ::_thesis: verum
end;
compatibility
for b1 being ManySortedFunction of product (doms f) holds
( b1 = Frege f iff for g being Function st g in product (doms f) holds
b1 . g = f .. g )
proof
let F be ManySortedFunction of product (doms f); ::_thesis: ( F = Frege f iff for g being Function st g in product (doms f) holds
F . g = f .. g )
for x being set holds
( x in rng f iff ( x in rng f & x is Function ) )
proof
let y be set ; ::_thesis: ( y in rng f iff ( y in rng f & y is Function ) )
( y in rng f implies y is Function )
proof
assume y in rng f ; ::_thesis: y is Function
then ex x being set st
( x in dom f & y = f . x ) by FUNCT_1:def_3;
hence y is Function ; ::_thesis: verum
end;
hence ( y in rng f iff ( y in rng f & y is Function ) ) ; ::_thesis: verum
end;
then A3: SubFuncs (rng f) = rng f by FUNCT_6:def_1;
thus ( F = Frege f implies for g being Function st g in product (doms f) holds
F . g = f .. g ) ::_thesis: ( ( for g being Function st g in product (doms f) holds
F . g = f .. g ) implies F = Frege f )
proof
assume A4: F = Frege f ; ::_thesis: for g being Function st g in product (doms f) holds
F . g = f .. g
let g be Function; ::_thesis: ( g in product (doms f) implies F . g = f .. g )
assume A5: g in product (doms f) ; ::_thesis: F . g = f .. g
then consider h being Function such that
A6: F . g = h and
A7: dom h = f " (SubFuncs (rng f)) and
A8: for x being set st x in dom h holds
h . x = (uncurry f) . (x,(g . x)) by A4, FUNCT_6:def_7;
A9: dom h = dom f by A3, A7, RELAT_1:134;
for x being set st x in dom f holds
h . x = (f . x) . (g . x)
proof
let x be set ; ::_thesis: ( x in dom f implies h . x = (f . x) . (g . x) )
assume A10: x in dom f ; ::_thesis: h . x = (f . x) . (g . x)
then x in dom (doms f) by A7, A9, FUNCT_6:def_2;
then g . x in (doms f) . x by A5, CARD_3:9;
then A11: g . x in dom (f . x) by A10, FUNCT_6:22;
thus h . x = f .. (x,(g . x)) by A8, A9, A10
.= (f . x) . (g . x) by A10, A11, FUNCT_5:38 ; ::_thesis: verum
end;
hence F . g = f .. g by A6, A9, PRALG_1:def_17; ::_thesis: verum
end;
assume A12: for g being Function st g in product (doms f) holds
F . g = f .. g ; ::_thesis: F = Frege f
A13: for g being Function st g in product (doms f) holds
ex h being Function st
( F . g = h & dom h = f " (SubFuncs (rng f)) & ( for x being set st x in dom h holds
h . x = (uncurry f) . (x,(g . x)) ) )
proof
let g be Function; ::_thesis: ( g in product (doms f) implies ex h being Function st
( F . g = h & dom h = f " (SubFuncs (rng f)) & ( for x being set st x in dom h holds
h . x = (uncurry f) . (x,(g . x)) ) ) )
assume A14: g in product (doms f) ; ::_thesis: ex h being Function st
( F . g = h & dom h = f " (SubFuncs (rng f)) & ( for x being set st x in dom h holds
h . x = (uncurry f) . (x,(g . x)) ) )
F . g = f .. g by A12, A14;
then A15: dom (F . g) = dom f by PRALG_1:def_17;
take F . g ; ::_thesis: ( F . g = F . g & dom (F . g) = f " (SubFuncs (rng f)) & ( for x being set st x in dom (F . g) holds
(F . g) . x = (uncurry f) . (x,(g . x)) ) )
thus F . g = F . g ; ::_thesis: ( dom (F . g) = f " (SubFuncs (rng f)) & ( for x being set st x in dom (F . g) holds
(F . g) . x = (uncurry f) . (x,(g . x)) ) )
thus A16: dom (F . g) = f " (SubFuncs (rng f)) by A3, A15, RELAT_1:134; ::_thesis: for x being set st x in dom (F . g) holds
(F . g) . x = (uncurry f) . (x,(g . x))
let x be set ; ::_thesis: ( x in dom (F . g) implies (F . g) . x = (uncurry f) . (x,(g . x)) )
assume A17: x in dom (F . g) ; ::_thesis: (F . g) . x = (uncurry f) . (x,(g . x))
then x in dom (doms f) by A16, FUNCT_6:def_2;
then g . x in (doms f) . x by A14, CARD_3:9;
then A18: g . x in dom (f . x) by A15, A17, FUNCT_6:22;
thus (F . g) . x = (f .. g) . x by A12, A14
.= (f . x) . (g . x) by A15, A17, PRALG_1:def_17
.= (uncurry f) . (x,(g . x)) by A15, A17, A18, FUNCT_5:38 ; ::_thesis: verum
end;
dom F = product (doms f) by PARTFUN1:def_2;
hence F = Frege f by A13, FUNCT_6:def_7; ::_thesis: verum
end;
end;
:: deftheorem Def2 defines Frege PRALG_2:def_2_:_
for f being Function-yielding Function
for b2 being ManySortedFunction of product (doms f) holds
( b2 = Frege f iff for g being Function st g in product (doms f) holds
b2 . g = f .. g );
registration
let I be set ;
let A, B be V2() ManySortedSet of I;
cluster[|A,B|] -> V2() ;
coherence
[|A,B|] is non-empty
proof
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
not_[|A,B|]_._i_is_empty
let i be set ; ::_thesis: ( i in I implies not [|A,B|] . i is empty )
assume A1: i in I ; ::_thesis: not [|A,B|] . i is empty
then [|A,B|] . i = [:(A . i),(B . i):] by PBOOLE:def_16;
hence not [|A,B|] . i is empty by A1, ZFMISC_1:90; ::_thesis: verum
end;
hence [|A,B|] is non-empty by PBOOLE:def_13; ::_thesis: verum
end;
end;
theorem :: PRALG_2:2
for I being non empty set
for J being set
for A, B being ManySortedSet of I
for f being Function of J,I holds [|A,B|] * f = [|(A * f),(B * f)|]
proof
let I be non empty set ; ::_thesis: for J being set
for A, B being ManySortedSet of I
for f being Function of J,I holds [|A,B|] * f = [|(A * f),(B * f)|]
let J be set ; ::_thesis: for A, B being ManySortedSet of I
for f being Function of J,I holds [|A,B|] * f = [|(A * f),(B * f)|]
let A, B be ManySortedSet of I; ::_thesis: for f being Function of J,I holds [|A,B|] * f = [|(A * f),(B * f)|]
let f be Function of J,I; ::_thesis: [|A,B|] * f = [|(A * f),(B * f)|]
for i being set st i in J holds
([|A,B|] * f) . i = [|(A * f),(B * f)|] . i
proof
A1: dom (B * f) = J by PARTFUN1:def_2;
let i be set ; ::_thesis: ( i in J implies ([|A,B|] * f) . i = [|(A * f),(B * f)|] . i )
A2: dom (A * f) = J by PARTFUN1:def_2;
assume A3: i in J ; ::_thesis: ([|A,B|] * f) . i = [|(A * f),(B * f)|] . i
then A4: f . i in I by FUNCT_2:5;
dom ([|A,B|] * f) = J by PARTFUN1:def_2;
hence ([|A,B|] * f) . i = [|A,B|] . (f . i) by A3, FUNCT_1:12
.= [:(A . (f . i)),(B . (f . i)):] by A4, PBOOLE:def_16
.= [:((A * f) . i),(B . (f . i)):] by A3, A2, FUNCT_1:12
.= [:((A * f) . i),((B * f) . i):] by A3, A1, FUNCT_1:12
.= [|(A * f),(B * f)|] . i by A3, PBOOLE:def_16 ;
::_thesis: verum
end;
hence [|A,B|] * f = [|(A * f),(B * f)|] by PBOOLE:3; ::_thesis: verum
end;
definition
let I be non empty set ;
let A, B be V2() ManySortedSet of I;
let pj be Element of I * ;
let rj be Element of I;
let f be Function of ((A #) . pj),(A . rj);
let g be Function of ((B #) . pj),(B . rj);
func[[:f,g:]] -> Function of (([|A,B|] #) . pj),([|A,B|] . rj) means :: PRALG_2:def 3
for h being Function st h in ([|A,B|] #) . pj holds
it . h = [(f . (pr1 h)),(g . (pr2 h))];
existence
ex b1 being Function of (([|A,B|] #) . pj),([|A,B|] . rj) st
for h being Function st h in ([|A,B|] #) . pj holds
b1 . h = [(f . (pr1 h)),(g . (pr2 h))]
proof
defpred S1[ set , set ] means for h being Function st h = $1 holds
$2 = [(f . (pr1 h)),(g . (pr2 h))];
set Y = [|A,B|] . rj;
set X = ([|A,B|] #) . pj;
A1: ([|A,B|] #) . pj = product ([|A,B|] * pj) by FINSEQ_2:def_5;
A2: for x being set st x in ([|A,B|] #) . pj holds
ex y being set st
( y in [|A,B|] . rj & S1[x,y] )
proof
let x be set ; ::_thesis: ( x in ([|A,B|] #) . pj implies ex y being set st
( y in [|A,B|] . rj & S1[x,y] ) )
A3: rng pj c= I by FINSEQ_1:def_4;
assume x in ([|A,B|] #) . pj ; ::_thesis: ex y being set st
( y in [|A,B|] . rj & S1[x,y] )
then consider h1 being Function such that
A4: h1 = x and
A5: dom h1 = dom ([|A,B|] * pj) and
A6: for z being set st z in dom ([|A,B|] * pj) holds
h1 . z in ([|A,B|] * pj) . z by A1, CARD_3:def_5;
A7: dom [|A,B|] = I by PARTFUN1:def_2;
then A8: dom h1 = dom pj by A5, A3, RELAT_1:27;
then A9: dom (pr1 h1) = dom pj by MCART_1:def_12;
dom A = I by PARTFUN1:def_2;
then A10: dom (pr1 h1) = dom (A * pj) by A3, A9, RELAT_1:27;
for z being set st z in dom (A * pj) holds
(pr1 h1) . z in (A * pj) . z
proof
let z be set ; ::_thesis: ( z in dom (A * pj) implies (pr1 h1) . z in (A * pj) . z )
assume A11: z in dom (A * pj) ; ::_thesis: (pr1 h1) . z in (A * pj) . z
dom ([|A,B|] * pj) = dom pj by A7, A3, RELAT_1:27;
then A12: ([|A,B|] * pj) . z = [|A,B|] . (pj . z) by A9, A10, A11, FUNCT_1:12;
( h1 . z in ([|A,B|] * pj) . z & pj . z in rng pj ) by A5, A6, A8, A9, A10, A11, FUNCT_1:def_3;
then h1 . z in [:(A . (pj . z)),(B . (pj . z)):] by A3, A12, PBOOLE:def_16;
then consider a, b being set such that
A13: a in A . (pj . z) and
b in B . (pj . z) and
A14: h1 . z = [a,b] by ZFMISC_1:def_2;
X: [a,b] `1 = a ;
(pr1 h1) . z = (h1 . z) `1 by A8, A9, A10, A11, MCART_1:def_12
.= a by A14, X ;
hence (pr1 h1) . z in (A * pj) . z by A11, A13, FUNCT_1:12; ::_thesis: verum
end;
then pr1 h1 in product (A * pj) by A10, CARD_3:9;
then pr1 h1 in (A #) . pj by FINSEQ_2:def_5;
then pr1 h1 in dom f by FUNCT_2:def_1;
then A15: f . (pr1 h1) in rng f by FUNCT_1:3;
take y = [(f . (pr1 h1)),(g . (pr2 h1))]; ::_thesis: ( y in [|A,B|] . rj & S1[x,y] )
( rng f c= A . rj & rng g c= B . rj ) by RELAT_1:def_19;
then A16: [:(rng f),(rng g):] c= [:(A . rj),(B . rj):] by ZFMISC_1:96;
A17: dom (pr2 h1) = dom pj by A8, MCART_1:def_13;
A18: dom B = I by PARTFUN1:def_2;
then A19: dom (pr2 h1) = dom (B * pj) by A3, A17, RELAT_1:27;
A20: for z being set st z in dom (B * pj) holds
(pr2 h1) . z in (B * pj) . z
proof
let z be set ; ::_thesis: ( z in dom (B * pj) implies (pr2 h1) . z in (B * pj) . z )
assume A21: z in dom (B * pj) ; ::_thesis: (pr2 h1) . z in (B * pj) . z
dom ([|A,B|] * pj) = dom pj by A7, A3, RELAT_1:27;
then A22: ([|A,B|] * pj) . z = [|A,B|] . (pj . z) by A17, A19, A21, FUNCT_1:12;
( h1 . z in ([|A,B|] * pj) . z & pj . z in rng pj ) by A5, A6, A8, A17, A19, A21, FUNCT_1:def_3;
then h1 . z in [:(A . (pj . z)),(B . (pj . z)):] by A3, A22, PBOOLE:def_16;
then consider a, b being set such that
a in A . (pj . z) and
A23: b in B . (pj . z) and
A24: h1 . z = [a,b] by ZFMISC_1:def_2;
X: [a,b] `2 = b ;
(pr2 h1) . z = (h1 . z) `2 by A8, A17, A19, A21, MCART_1:def_13
.= b by A24, X ;
hence (pr2 h1) . z in (B * pj) . z by A21, A23, FUNCT_1:12; ::_thesis: verum
end;
dom (pr2 h1) = dom pj by A8, MCART_1:def_13;
then dom (pr2 h1) = dom (B * pj) by A18, A3, RELAT_1:27;
then pr2 h1 in product (B * pj) by A20, CARD_3:9;
then pr2 h1 in (B #) . pj by FINSEQ_2:def_5;
then pr2 h1 in dom g by FUNCT_2:def_1;
then g . (pr2 h1) in rng g by FUNCT_1:3;
then [(f . (pr1 h1)),(g . (pr2 h1))] in [:(rng f),(rng g):] by A15, ZFMISC_1:87;
then [(f . (pr1 h1)),(g . (pr2 h1))] in [:(A . rj),(B . rj):] by A16;
hence y in [|A,B|] . rj by PBOOLE:def_16; ::_thesis: S1[x,y]
let h be Function; ::_thesis: ( h = x implies y = [(f . (pr1 h)),(g . (pr2 h))] )
assume x = h ; ::_thesis: y = [(f . (pr1 h)),(g . (pr2 h))]
hence y = [(f . (pr1 h)),(g . (pr2 h))] by A4; ::_thesis: verum
end;
consider F being Function of (([|A,B|] #) . pj),([|A,B|] . rj) such that
A25: for x being set st x in ([|A,B|] #) . pj holds
S1[x,F . x] from FUNCT_2:sch_1(A2);
take F ; ::_thesis: for h being Function st h in ([|A,B|] #) . pj holds
F . h = [(f . (pr1 h)),(g . (pr2 h))]
thus for h being Function st h in ([|A,B|] #) . pj holds
F . h = [(f . (pr1 h)),(g . (pr2 h))] by A25; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of (([|A,B|] #) . pj),([|A,B|] . rj) st ( for h being Function st h in ([|A,B|] #) . pj holds
b1 . h = [(f . (pr1 h)),(g . (pr2 h))] ) & ( for h being Function st h in ([|A,B|] #) . pj holds
b2 . h = [(f . (pr1 h)),(g . (pr2 h))] ) holds
b1 = b2
proof
let x, y be Function of (([|A,B|] #) . pj),([|A,B|] . rj); ::_thesis: ( ( for h being Function st h in ([|A,B|] #) . pj holds
x . h = [(f . (pr1 h)),(g . (pr2 h))] ) & ( for h being Function st h in ([|A,B|] #) . pj holds
y . h = [(f . (pr1 h)),(g . (pr2 h))] ) implies x = y )
assume that
A26: for h being Function st h in ([|A,B|] #) . pj holds
x . h = [(f . (pr1 h)),(g . (pr2 h))] and
A27: for h being Function st h in ([|A,B|] #) . pj holds
y . h = [(f . (pr1 h)),(g . (pr2 h))] ; ::_thesis: x = y
let h be Element of ([|A,B|] #) . pj; :: according to FUNCT_2:def_8 ::_thesis: x . h = y . h
h in ([|A,B|] #) . pj ;
then h in product ([|A,B|] * pj) by FINSEQ_2:def_5;
then consider h1 being Function such that
A28: h1 = h and
dom h1 = dom ([|A,B|] * pj) and
for z being set st z in dom ([|A,B|] * pj) holds
h1 . z in ([|A,B|] * pj) . z by CARD_3:def_5;
x . h1 = [(f . (pr1 h1)),(g . (pr2 h1))] by A26, A28;
hence x . h = y . h by A27, A28; ::_thesis: verum
end;
end;
:: deftheorem defines [[: PRALG_2:def_3_:_
for I being non empty set
for A, B being V2() ManySortedSet of I
for pj being Element of I *
for rj being Element of I
for f being Function of ((A #) . pj),(A . rj)
for g being Function of ((B #) . pj),(B . rj)
for b8 being Function of (([|A,B|] #) . pj),([|A,B|] . rj) holds
( b8 = [[:f,g:]] iff for h being Function st h in ([|A,B|] #) . pj holds
b8 . h = [(f . (pr1 h)),(g . (pr2 h))] );
definition
let I be non empty set ;
let J be set ;
let A, B be V2() ManySortedSet of I;
let p be Function of J,(I *);
let r be Function of J,I;
let F be ManySortedFunction of (A #) * p,A * r;
let G be ManySortedFunction of (B #) * p,B * r;
func[[:F,G:]] -> ManySortedFunction of ([|A,B|] #) * p,[|A,B|] * r means :: PRALG_2:def 4
for j being set st j in J holds
for pj being Element of I *
for rj being Element of I st pj = p . j & rj = r . j holds
for f being Function of ((A #) . pj),(A . rj)
for g being Function of ((B #) . pj),(B . rj) st f = F . j & g = G . j holds
it . j = [[:f,g:]];
existence
ex b1 being ManySortedFunction of ([|A,B|] #) * p,[|A,B|] * r st
for j being set st j in J holds
for pj being Element of I *
for rj being Element of I st pj = p . j & rj = r . j holds
for f being Function of ((A #) . pj),(A . rj)
for g being Function of ((B #) . pj),(B . rj) st f = F . j & g = G . j holds
b1 . j = [[:f,g:]]
proof
defpred S1[ set , set ] means for pj being Element of I *
for rj being Element of I st pj = p . $1 & rj = r . $1 holds
for f being Function of ((A #) . pj),(A . rj)
for g being Function of ((B #) . pj),(B . rj) st f = F . $1 & g = G . $1 holds
$2 = [[:f,g:]];
A1: for j being set st j in J holds
ex i being set st S1[j,i]
proof
let j be set ; ::_thesis: ( j in J implies ex i being set st S1[j,i] )
assume A2: j in J ; ::_thesis: ex i being set st S1[j,i]
then reconsider pj = p . j as Element of I * by FUNCT_2:5;
reconsider rj = r . j as Element of I by A2, FUNCT_2:5;
A3: j in dom r by A2, FUNCT_2:def_1;
then A4: A . (r . j) = (A * r) . j by FUNCT_1:13;
A5: B . (r . j) = (B * r) . j by A3, FUNCT_1:13;
A6: j in dom p by A2, FUNCT_2:def_1;
then (A #) . (p . j) = ((A #) * p) . j by FUNCT_1:13;
then reconsider f = F . j as Function of ((A #) . pj),(A . rj) by A2, A4, PBOOLE:def_15;
(B #) . (p . j) = ((B #) * p) . j by A6, FUNCT_1:13;
then reconsider g = G . j as Function of ((B #) . pj),(B . rj) by A2, A5, PBOOLE:def_15;
take [[:f,g:]] ; ::_thesis: S1[j,[[:f,g:]]]
thus S1[j,[[:f,g:]]] ; ::_thesis: verum
end;
consider h being Function such that
A7: ( dom h = J & ( for j being set st j in J holds
S1[j,h . j] ) ) from CLASSES1:sch_1(A1);
reconsider h = h as ManySortedSet of J by A7, PARTFUN1:def_2, RELAT_1:def_18;
for j being set st j in dom h holds
h . j is Function
proof
let j be set ; ::_thesis: ( j in dom h implies h . j is Function )
assume A8: j in dom h ; ::_thesis: h . j is Function
then reconsider pj = p . j as Element of I * by A7, FUNCT_2:5;
reconsider rj = r . j as Element of I by A7, A8, FUNCT_2:5;
A9: j in dom r by A7, A8, FUNCT_2:def_1;
then A10: A . (r . j) = (A * r) . j by FUNCT_1:13;
A11: B . (r . j) = (B * r) . j by A9, FUNCT_1:13;
A12: j in dom p by A7, A8, FUNCT_2:def_1;
then (A #) . (p . j) = ((A #) * p) . j by FUNCT_1:13;
then reconsider f = F . j as Function of ((A #) . pj),(A . rj) by A7, A8, A10, PBOOLE:def_15;
(B #) . (p . j) = ((B #) * p) . j by A12, FUNCT_1:13;
then reconsider g = G . j as Function of ((B #) . pj),(B . rj) by A7, A8, A11, PBOOLE:def_15;
h . j = [[:f,g:]] by A7, A8;
hence h . j is Function ; ::_thesis: verum
end;
then reconsider h = h as ManySortedFunction of J by FUNCOP_1:def_6;
for j being set st j in J holds
h . j is Function of ((([|A,B|] #) * p) . j),(([|A,B|] * r) . j)
proof
let j be set ; ::_thesis: ( j in J implies h . j is Function of ((([|A,B|] #) * p) . j),(([|A,B|] * r) . j) )
assume A13: j in J ; ::_thesis: h . j is Function of ((([|A,B|] #) * p) . j),(([|A,B|] * r) . j)
then reconsider pj = p . j as Element of I * by FUNCT_2:5;
reconsider rj = r . j as Element of I by A13, FUNCT_2:5;
A14: j in dom p by A13, FUNCT_2:def_1;
then A15: (([|A,B|] #) * p) . j = ([|A,B|] #) . (p . j) by FUNCT_1:13;
A16: j in dom r by A13, FUNCT_2:def_1;
then A17: A . (r . j) = (A * r) . j by FUNCT_1:13;
A18: ([|A,B|] * r) . j = [|A,B|] . (r . j) by A16, FUNCT_1:13;
A19: B . (r . j) = (B * r) . j by A16, FUNCT_1:13;
(B #) . (p . j) = ((B #) * p) . j by A14, FUNCT_1:13;
then reconsider g = G . j as Function of ((B #) . pj),(B . rj) by A13, A19, PBOOLE:def_15;
(A #) . (p . j) = ((A #) * p) . j by A14, FUNCT_1:13;
then reconsider f = F . j as Function of ((A #) . pj),(A . rj) by A13, A17, PBOOLE:def_15;
h . j = [[:f,g:]] by A7, A13;
hence h . j is Function of ((([|A,B|] #) * p) . j),(([|A,B|] * r) . j) by A15, A18; ::_thesis: verum
end;
then reconsider h = h as ManySortedFunction of ([|A,B|] #) * p,[|A,B|] * r by PBOOLE:def_15;
take h ; ::_thesis: for j being set st j in J holds
for pj being Element of I *
for rj being Element of I st pj = p . j & rj = r . j holds
for f being Function of ((A #) . pj),(A . rj)
for g being Function of ((B #) . pj),(B . rj) st f = F . j & g = G . j holds
h . j = [[:f,g:]]
thus for j being set st j in J holds
for pj being Element of I *
for rj being Element of I st pj = p . j & rj = r . j holds
for f being Function of ((A #) . pj),(A . rj)
for g being Function of ((B #) . pj),(B . rj) st f = F . j & g = G . j holds
h . j = [[:f,g:]] by A7; ::_thesis: verum
end;
uniqueness
for b1, b2 being ManySortedFunction of ([|A,B|] #) * p,[|A,B|] * r st ( for j being set st j in J holds
for pj being Element of I *
for rj being Element of I st pj = p . j & rj = r . j holds
for f being Function of ((A #) . pj),(A . rj)
for g being Function of ((B #) . pj),(B . rj) st f = F . j & g = G . j holds
b1 . j = [[:f,g:]] ) & ( for j being set st j in J holds
for pj being Element of I *
for rj being Element of I st pj = p . j & rj = r . j holds
for f being Function of ((A #) . pj),(A . rj)
for g being Function of ((B #) . pj),(B . rj) st f = F . j & g = G . j holds
b2 . j = [[:f,g:]] ) holds
b1 = b2
proof
let x, y be ManySortedFunction of ([|A,B|] #) * p,[|A,B|] * r; ::_thesis: ( ( for j being set st j in J holds
for pj being Element of I *
for rj being Element of I st pj = p . j & rj = r . j holds
for f being Function of ((A #) . pj),(A . rj)
for g being Function of ((B #) . pj),(B . rj) st f = F . j & g = G . j holds
x . j = [[:f,g:]] ) & ( for j being set st j in J holds
for pj being Element of I *
for rj being Element of I st pj = p . j & rj = r . j holds
for f being Function of ((A #) . pj),(A . rj)
for g being Function of ((B #) . pj),(B . rj) st f = F . j & g = G . j holds
y . j = [[:f,g:]] ) implies x = y )
assume that
A20: for j being set st j in J holds
for pj being Element of I *
for rj being Element of I st pj = p . j & rj = r . j holds
for f being Function of ((A #) . pj),(A . rj)
for g being Function of ((B #) . pj),(B . rj) st f = F . j & g = G . j holds
x . j = [[:f,g:]] and
A21: for j being set st j in J holds
for pj being Element of I *
for rj being Element of I st pj = p . j & rj = r . j holds
for f being Function of ((A #) . pj),(A . rj)
for g being Function of ((B #) . pj),(B . rj) st f = F . j & g = G . j holds
y . j = [[:f,g:]] ; ::_thesis: x = y
for j being set st j in J holds
x . j = y . j
proof
let j be set ; ::_thesis: ( j in J implies x . j = y . j )
assume A22: j in J ; ::_thesis: x . j = y . j
then reconsider pj = p . j as Element of I * by FUNCT_2:5;
reconsider rj = r . j as Element of I by A22, FUNCT_2:5;
A23: j in dom r by A22, FUNCT_2:def_1;
then A24: A . (r . j) = (A * r) . j by FUNCT_1:13;
A25: B . (r . j) = (B * r) . j by A23, FUNCT_1:13;
A26: j in dom p by A22, FUNCT_2:def_1;
then (A #) . (p . j) = ((A #) * p) . j by FUNCT_1:13;
then reconsider f = F . j as Function of ((A #) . pj),(A . rj) by A22, A24, PBOOLE:def_15;
(B #) . (p . j) = ((B #) * p) . j by A26, FUNCT_1:13;
then reconsider g = G . j as Function of ((B #) . pj),(B . rj) by A22, A25, PBOOLE:def_15;
x . j = [[:f,g:]] by A20, A22;
hence x . j = y . j by A21, A22; ::_thesis: verum
end;
hence x = y by PBOOLE:3; ::_thesis: verum
end;
end;
:: deftheorem defines [[: PRALG_2:def_4_:_
for I being non empty set
for J being set
for A, B being V2() ManySortedSet of I
for p being Function of J,(I *)
for r being Function of J,I
for F being ManySortedFunction of (A #) * p,A * r
for G being ManySortedFunction of (B #) * p,B * r
for b9 being ManySortedFunction of ([|A,B|] #) * p,[|A,B|] * r holds
( b9 = [[:F,G:]] iff for j being set st j in J holds
for pj being Element of I *
for rj being Element of I st pj = p . j & rj = r . j holds
for f being Function of ((A #) . pj),(A . rj)
for g being Function of ((B #) . pj),(B . rj) st f = F . j & g = G . j holds
b9 . j = [[:f,g:]] );
begin
definition
let I be set ;
let S be non empty ManySortedSign ;
mode MSAlgebra-Family of I,S -> ManySortedSet of I means :Def5: :: PRALG_2:def 5
for i being set st i in I holds
it . i is non-empty MSAlgebra over S;
existence
ex b1 being ManySortedSet of I st
for i being set st i in I holds
b1 . i is non-empty MSAlgebra over S
proof
set A = the non-empty MSAlgebra over S;
set f = I --> the non-empty MSAlgebra over S;
reconsider f = I --> the non-empty MSAlgebra over S as ManySortedSet of I ;
take f ; ::_thesis: for i being set st i in I holds
f . i is non-empty MSAlgebra over S
let i be set ; ::_thesis: ( i in I implies f . i is non-empty MSAlgebra over S )
assume i in I ; ::_thesis: f . i is non-empty MSAlgebra over S
hence f . i is non-empty MSAlgebra over S by FUNCOP_1:7; ::_thesis: verum
end;
end;
:: deftheorem Def5 defines MSAlgebra-Family PRALG_2:def_5_:_
for I being set
for S being non empty ManySortedSign
for b3 being ManySortedSet of I holds
( b3 is MSAlgebra-Family of I,S iff for i being set st i in I holds
b3 . i is non-empty MSAlgebra over S );
definition
let I be non empty set ;
let S be non empty ManySortedSign ;
let A be MSAlgebra-Family of I,S;
let i be Element of I;
:: original: .
redefine funcA . i -> non-empty MSAlgebra over S;
coherence
A . i is non-empty MSAlgebra over S by Def5;
end;
definition
let S be non empty ManySortedSign ;
let U1 be MSAlgebra over S;
func|.U1.| -> set equals :: PRALG_2:def 6
union (rng the Sorts of U1);
coherence
union (rng the Sorts of U1) is set ;
end;
:: deftheorem defines |. PRALG_2:def_6_:_
for S being non empty ManySortedSign
for U1 being MSAlgebra over S holds |.U1.| = union (rng the Sorts of U1);
registration
let S be non empty ManySortedSign ;
let U1 be non-empty MSAlgebra over S;
cluster|.U1.| -> non empty ;
coherence
not |.U1.| is empty
proof
reconsider St = the Sorts of U1 as V2() ManySortedSet of the carrier of S ;
set s = the SortSymbol of S;
dom the Sorts of U1 = the carrier of S by PARTFUN1:def_2;
then A1: the Sorts of U1 . the SortSymbol of S in rng the Sorts of U1 by FUNCT_1:def_3;
ex x being set st x in St . the SortSymbol of S by XBOOLE_0:def_1;
hence not |.U1.| is empty by A1, TARSKI:def_4; ::_thesis: verum
end;
end;
definition
let I be non empty set ;
let S be non empty ManySortedSign ;
let A be MSAlgebra-Family of I,S;
func|.A.| -> set equals :: PRALG_2:def 7
union { |.(A . i).| where i is Element of I : verum } ;
coherence
union { |.(A . i).| where i is Element of I : verum } is set ;
end;
:: deftheorem defines |. PRALG_2:def_7_:_
for I being non empty set
for S being non empty ManySortedSign
for A being MSAlgebra-Family of I,S holds |.A.| = union { |.(A . i).| where i is Element of I : verum } ;
registration
let I be non empty set ;
let S be non empty ManySortedSign ;
let A be MSAlgebra-Family of I,S;
cluster|.A.| -> non empty ;
coherence
not |.A.| is empty
proof
set a = the Element of I;
set X = { |.(A . i).| where i is Element of I : verum } ;
( |.(A . the Element of I).| in { |.(A . i).| where i is Element of I : verum } & ex x being set st x in |.(A . the Element of I).| ) by XBOOLE_0:def_1;
hence not |.A.| is empty by TARSKI:def_4; ::_thesis: verum
end;
end;
begin
theorem Th3: :: PRALG_2:3
for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for o being OperSymbol of S holds
( Args (o,U0) = product ( the Sorts of U0 * (the_arity_of o)) & dom ( the Sorts of U0 * (the_arity_of o)) = dom (the_arity_of o) & Result (o,U0) = the Sorts of U0 . (the_result_sort_of o) )
proof
let S be non empty non void ManySortedSign ; ::_thesis: for U0 being MSAlgebra over S
for o being OperSymbol of S holds
( Args (o,U0) = product ( the Sorts of U0 * (the_arity_of o)) & dom ( the Sorts of U0 * (the_arity_of o)) = dom (the_arity_of o) & Result (o,U0) = the Sorts of U0 . (the_result_sort_of o) )
let U0 be MSAlgebra over S; ::_thesis: for o being OperSymbol of S holds
( Args (o,U0) = product ( the Sorts of U0 * (the_arity_of o)) & dom ( the Sorts of U0 * (the_arity_of o)) = dom (the_arity_of o) & Result (o,U0) = the Sorts of U0 . (the_result_sort_of o) )
let o be OperSymbol of S; ::_thesis: ( Args (o,U0) = product ( the Sorts of U0 * (the_arity_of o)) & dom ( the Sorts of U0 * (the_arity_of o)) = dom (the_arity_of o) & Result (o,U0) = the Sorts of U0 . (the_result_sort_of o) )
set So = the Sorts of U0;
set Ar = the Arity of S;
set Rs = the ResultSort of S;
set ar = the_arity_of o;
set AS = ( the Sorts of U0 #) * the Arity of S;
set RS = the Sorts of U0 * the ResultSort of S;
set X = the carrier' of S;
set Cr = the carrier of S;
A1: dom the Arity of S = the carrier' of S by FUNCT_2:def_1;
then A2: dom (( the Sorts of U0 #) * the Arity of S) = dom the Arity of S by PARTFUN1:def_2;
thus Args (o,U0) = (( the Sorts of U0 #) * the Arity of S) . o by MSUALG_1:def_4
.= ( the Sorts of U0 #) . ( the Arity of S . o) by A1, A2, FUNCT_1:12
.= ( the Sorts of U0 #) . (the_arity_of o) by MSUALG_1:def_1
.= product ( the Sorts of U0 * (the_arity_of o)) by FINSEQ_2:def_5 ; ::_thesis: ( dom ( the Sorts of U0 * (the_arity_of o)) = dom (the_arity_of o) & Result (o,U0) = the Sorts of U0 . (the_result_sort_of o) )
( rng (the_arity_of o) c= the carrier of S & dom the Sorts of U0 = the carrier of S ) by FINSEQ_1:def_4, PARTFUN1:def_2;
hence dom ( the Sorts of U0 * (the_arity_of o)) = dom (the_arity_of o) by RELAT_1:27; ::_thesis: Result (o,U0) = the Sorts of U0 . (the_result_sort_of o)
A3: dom the ResultSort of S = the carrier' of S by FUNCT_2:def_1;
then A4: dom ( the Sorts of U0 * the ResultSort of S) = dom the ResultSort of S by PARTFUN1:def_2;
thus Result (o,U0) = ( the Sorts of U0 * the ResultSort of S) . o by MSUALG_1:def_5
.= the Sorts of U0 . ( the ResultSort of S . o) by A3, A4, FUNCT_1:12
.= the Sorts of U0 . (the_result_sort_of o) by MSUALG_1:def_2 ; ::_thesis: verum
end;
theorem Th4: :: PRALG_2:4
for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for o being OperSymbol of S st the_arity_of o = {} holds
Args (o,U0) = {{}}
proof
let S be non empty non void ManySortedSign ; ::_thesis: for U0 being MSAlgebra over S
for o being OperSymbol of S st the_arity_of o = {} holds
Args (o,U0) = {{}}
let U0 be MSAlgebra over S; ::_thesis: for o being OperSymbol of S st the_arity_of o = {} holds
Args (o,U0) = {{}}
let o be OperSymbol of S; ::_thesis: ( the_arity_of o = {} implies Args (o,U0) = {{}} )
assume A1: the_arity_of o = {} ; ::_thesis: Args (o,U0) = {{}}
thus Args (o,U0) = product ( the Sorts of U0 * (the_arity_of o)) by Th3
.= {{}} by A1, CARD_3:10 ; ::_thesis: verum
end;
definition
let S be non empty ManySortedSign ;
let U1, U2 be non-empty MSAlgebra over S;
func[:U1,U2:] -> MSAlgebra over S equals :: PRALG_2:def 8
MSAlgebra(# [| the Sorts of U1, the Sorts of U2|],[[: the Charact of U1, the Charact of U2:]] #);
coherence
MSAlgebra(# [| the Sorts of U1, the Sorts of U2|],[[: the Charact of U1, the Charact of U2:]] #) is MSAlgebra over S ;
end;
:: deftheorem defines [: PRALG_2:def_8_:_
for S being non empty ManySortedSign
for U1, U2 being non-empty MSAlgebra over S holds [:U1,U2:] = MSAlgebra(# [| the Sorts of U1, the Sorts of U2|],[[: the Charact of U1, the Charact of U2:]] #);
registration
let S be non empty ManySortedSign ;
let U1, U2 be non-empty MSAlgebra over S;
cluster[:U1,U2:] -> strict ;
coherence
[:U1,U2:] is strict ;
end;
definition
let I be set ;
let S be non empty ManySortedSign ;
let s be SortSymbol of S;
let A be MSAlgebra-Family of I,S;
func Carrier (A,s) -> ManySortedSet of I means :Def9: :: PRALG_2:def 9
for i being set st i in I holds
ex U0 being MSAlgebra over S st
( U0 = A . i & it . i = the Sorts of U0 . s ) if I <> {}
otherwise it = {} ;
existence
( ( I <> {} implies ex b1 being ManySortedSet of I st
for i being set st i in I holds
ex U0 being MSAlgebra over S st
( U0 = A . i & b1 . i = the Sorts of U0 . s ) ) & ( not I <> {} implies ex b1 being ManySortedSet of I st b1 = {} ) )
proof
hereby ::_thesis: ( not I <> {} implies ex b1 being ManySortedSet of I st b1 = {} )
assume I <> {} ; ::_thesis: ex f being ManySortedSet of I st
for i being set st i in I holds
ex U0 being MSAlgebra over S st
( U0 = A . i & f . i = the Sorts of U0 . s )
then reconsider I9 = I as non empty set ;
reconsider A9 = A as MSAlgebra-Family of I9,S ;
deffunc H1( Element of I9) -> set = the Sorts of (A9 . $1) . s;
consider f being Function such that
A1: ( dom f = I9 & ( for i being Element of I9 holds f . i = H1(i) ) ) from FUNCT_1:sch_4();
reconsider f = f as ManySortedSet of I by A1, PARTFUN1:def_2, RELAT_1:def_18;
take f = f; ::_thesis: for i being set st i in I holds
ex U0 being MSAlgebra over S st
( U0 = A . i & f . i = the Sorts of U0 . s )
let i be set ; ::_thesis: ( i in I implies ex U0 being MSAlgebra over S st
( U0 = A . i & f . i = the Sorts of U0 . s ) )
assume i in I ; ::_thesis: ex U0 being MSAlgebra over S st
( U0 = A . i & f . i = the Sorts of U0 . s )
then reconsider i9 = i as Element of I9 ;
reconsider U0 = A9 . i9 as MSAlgebra over S ;
take U0 = U0; ::_thesis: ( U0 = A . i & f . i = the Sorts of U0 . s )
thus ( U0 = A . i & f . i = the Sorts of U0 . s ) by A1; ::_thesis: verum
end;
assume A2: I = {} ; ::_thesis: ex b1 being ManySortedSet of I st b1 = {}
take [[0]] I ; ::_thesis: [[0]] I = {}
thus [[0]] I = {} by A2; ::_thesis: verum
end;
uniqueness
for b1, b2 being ManySortedSet of I holds
( ( I <> {} & ( for i being set st i in I holds
ex U0 being MSAlgebra over S st
( U0 = A . i & b1 . i = the Sorts of U0 . s ) ) & ( for i being set st i in I holds
ex U0 being MSAlgebra over S st
( U0 = A . i & b2 . i = the Sorts of U0 . s ) ) implies b1 = b2 ) & ( not I <> {} & b1 = {} & b2 = {} implies b1 = b2 ) )
proof
let f, g be ManySortedSet of I; ::_thesis: ( ( I <> {} & ( for i being set st i in I holds
ex U0 being MSAlgebra over S st
( U0 = A . i & f . i = the Sorts of U0 . s ) ) & ( for i being set st i in I holds
ex U0 being MSAlgebra over S st
( U0 = A . i & g . i = the Sorts of U0 . s ) ) implies f = g ) & ( not I <> {} & f = {} & g = {} implies f = g ) )
hereby ::_thesis: ( not I <> {} & f = {} & g = {} implies f = g )
assume I <> {} ; ::_thesis: ( ( for i being set st i in I holds
ex U0 being MSAlgebra over S st
( U0 = A . i & f . i = the Sorts of U0 . s ) ) & ( for i being set st i in I holds
ex U0 being MSAlgebra over S st
( U0 = A . i & g . i = the Sorts of U0 . s ) ) implies f = g )
assume A3: ( ( for i being set st i in I holds
ex U0 being MSAlgebra over S st
( U0 = A . i & f . i = the Sorts of U0 . s ) ) & ( for i being set st i in I holds
ex U0 being MSAlgebra over S st
( U0 = A . i & g . i = the Sorts of U0 . s ) ) ) ; ::_thesis: f = g
for x being set st x in I holds
f . x = g . x
proof
let x be set ; ::_thesis: ( x in I implies f . x = g . x )
assume A4: x in I ; ::_thesis: f . x = g . x
then reconsider i = x as Element of I ;
( ex U0 being MSAlgebra over S st
( U0 = A . i & f . i = the Sorts of U0 . s ) & ex U0 being MSAlgebra over S st
( U0 = A . i & g . i = the Sorts of U0 . s ) ) by A3, A4;
hence f . x = g . x ; ::_thesis: verum
end;
hence f = g by PBOOLE:3; ::_thesis: verum
end;
thus ( not I <> {} & f = {} & g = {} implies f = g ) ; ::_thesis: verum
end;
correctness
consistency
for b1 being ManySortedSet of I holds verum;
;
end;
:: deftheorem Def9 defines Carrier PRALG_2:def_9_:_
for I being set
for S being non empty ManySortedSign
for s being SortSymbol of S
for A being MSAlgebra-Family of I,S
for b5 being ManySortedSet of I holds
( ( I <> {} implies ( b5 = Carrier (A,s) iff for i being set st i in I holds
ex U0 being MSAlgebra over S st
( U0 = A . i & b5 . i = the Sorts of U0 . s ) ) ) & ( not I <> {} implies ( b5 = Carrier (A,s) iff b5 = {} ) ) );
registration
let I be set ;
let S be non empty ManySortedSign ;
let s be SortSymbol of S;
let A be MSAlgebra-Family of I,S;
cluster Carrier (A,s) -> V2() ;
coherence
Carrier (A,s) is non-empty
proof
let x be set ; :: according to PBOOLE:def_13 ::_thesis: ( not x in I or not (Carrier (A,s)) . x is empty )
assume A1: x in I ; ::_thesis: not (Carrier (A,s)) . x is empty
then consider U0 being MSAlgebra over S such that
A2: U0 = A . x and
A3: (Carrier (A,s)) . x = the Sorts of U0 . s by Def9;
U0 is non-empty MSAlgebra over S by A1, A2, Def5;
hence not (Carrier (A,s)) . x is empty by A3; ::_thesis: verum
end;
end;
definition
let I be set ;
let S be non empty ManySortedSign ;
let A be MSAlgebra-Family of I,S;
func SORTS A -> ManySortedSet of the carrier of S means :Def10: :: PRALG_2:def 10
for s being SortSymbol of S holds it . s = product (Carrier (A,s));
existence
ex b1 being ManySortedSet of the carrier of S st
for s being SortSymbol of S holds b1 . s = product (Carrier (A,s))
proof
deffunc H1( SortSymbol of S) -> set = product (Carrier (A,$1));
consider f being Function such that
A1: ( dom f = the carrier of S & ( for s being SortSymbol of S holds f . s = H1(s) ) ) from FUNCT_1:sch_4();
reconsider f = f as ManySortedSet of the carrier of S by A1, PARTFUN1:def_2, RELAT_1:def_18;
take f ; ::_thesis: for s being SortSymbol of S holds f . s = product (Carrier (A,s))
thus for s being SortSymbol of S holds f . s = product (Carrier (A,s)) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being ManySortedSet of the carrier of S st ( for s being SortSymbol of S holds b1 . s = product (Carrier (A,s)) ) & ( for s being SortSymbol of S holds b2 . s = product (Carrier (A,s)) ) holds
b1 = b2
proof
let f, g be ManySortedSet of the carrier of S; ::_thesis: ( ( for s being SortSymbol of S holds f . s = product (Carrier (A,s)) ) & ( for s being SortSymbol of S holds g . s = product (Carrier (A,s)) ) implies f = g )
assume that
A2: for s being SortSymbol of S holds f . s = product (Carrier (A,s)) and
A3: for s being SortSymbol of S holds g . s = product (Carrier (A,s)) ; ::_thesis: f = g
for x being set st x in the carrier of S holds
f . x = g . x
proof
let x be set ; ::_thesis: ( x in the carrier of S implies f . x = g . x )
assume x in the carrier of S ; ::_thesis: f . x = g . x
then reconsider x1 = x as SortSymbol of S ;
f . x1 = product (Carrier (A,x1)) by A2;
hence f . x = g . x by A3; ::_thesis: verum
end;
hence f = g by PBOOLE:3; ::_thesis: verum
end;
end;
:: deftheorem Def10 defines SORTS PRALG_2:def_10_:_
for I being set
for S being non empty ManySortedSign
for A being MSAlgebra-Family of I,S
for b4 being ManySortedSet of the carrier of S holds
( b4 = SORTS A iff for s being SortSymbol of S holds b4 . s = product (Carrier (A,s)) );
registration
let I be set ;
let S be non empty ManySortedSign ;
let A be MSAlgebra-Family of I,S;
cluster SORTS A -> V2() ;
coherence
SORTS A is non-empty
proof
let x be set ; :: according to PBOOLE:def_13 ::_thesis: ( not x in the carrier of S or not (SORTS A) . x is empty )
assume x in the carrier of S ; ::_thesis: not (SORTS A) . x is empty
then reconsider s = x as SortSymbol of S ;
(SORTS A) . s = product (Carrier (A,s)) by Def10;
hence not (SORTS A) . x is empty ; ::_thesis: verum
end;
end;
definition
let I be set ;
let S be non empty ManySortedSign ;
let A be MSAlgebra-Family of I,S;
func OPER A -> ManySortedFunction of I means :Def11: :: PRALG_2:def 11
for i being set st i in I holds
ex U0 being MSAlgebra over S st
( U0 = A . i & it . i = the Charact of U0 ) if I <> {}
otherwise it = {} ;
existence
( ( I <> {} implies ex b1 being ManySortedFunction of I st
for i being set st i in I holds
ex U0 being MSAlgebra over S st
( U0 = A . i & b1 . i = the Charact of U0 ) ) & ( not I <> {} implies ex b1 being ManySortedFunction of I st b1 = {} ) )
proof
reconsider f = [[0]] I as ManySortedFunction of I ;
hereby ::_thesis: ( not I <> {} implies ex b1 being ManySortedFunction of I st b1 = {} )
assume I <> {} ; ::_thesis: ex X being ManySortedFunction of I st
for i being set st i in I holds
ex U0 being MSAlgebra over S st
( U0 = A . i & X . i = the Charact of U0 )
then reconsider I9 = I as non empty set ;
reconsider A9 = A as MSAlgebra-Family of I9,S ;
deffunc H1( Element of I9) -> ManySortedFunction of the Arity of S * ( the Sorts of (A9 . $1) #), the ResultSort of S * the Sorts of (A9 . $1) = the Charact of (A9 . $1);
consider X being ManySortedSet of I9 such that
A1: for i being Element of I9 holds X . i = H1(i) from PBOOLE:sch_5();
for x being set st x in dom X holds
X . x is Function
proof
let x be set ; ::_thesis: ( x in dom X implies X . x is Function )
assume x in dom X ; ::_thesis: X . x is Function
then reconsider i = x as Element of I9 by PARTFUN1:def_2;
X . i = the Charact of (A9 . i) by A1;
hence X . x is Function ; ::_thesis: verum
end;
then reconsider X = X as ManySortedFunction of I by FUNCOP_1:def_6;
take X = X; ::_thesis: for i being set st i in I holds
ex U0 being MSAlgebra over S st
( U0 = A . i & X . i = the Charact of U0 )
let i be set ; ::_thesis: ( i in I implies ex U0 being MSAlgebra over S st
( U0 = A . i & X . i = the Charact of U0 ) )
assume i in I ; ::_thesis: ex U0 being MSAlgebra over S st
( U0 = A . i & X . i = the Charact of U0 )
then reconsider i9 = i as Element of I9 ;
reconsider U0 = A9 . i9 as MSAlgebra over S ;
take U0 = U0; ::_thesis: ( U0 = A . i & X . i = the Charact of U0 )
thus ( U0 = A . i & X . i = the Charact of U0 ) by A1; ::_thesis: verum
end;
assume A2: I = {} ; ::_thesis: ex b1 being ManySortedFunction of I st b1 = {}
take f ; ::_thesis: f = {}
thus f = {} by A2; ::_thesis: verum
end;
uniqueness
for b1, b2 being ManySortedFunction of I holds
( ( I <> {} & ( for i being set st i in I holds
ex U0 being MSAlgebra over S st
( U0 = A . i & b1 . i = the Charact of U0 ) ) & ( for i being set st i in I holds
ex U0 being MSAlgebra over S st
( U0 = A . i & b2 . i = the Charact of U0 ) ) implies b1 = b2 ) & ( not I <> {} & b1 = {} & b2 = {} implies b1 = b2 ) )
proof
let f, g be ManySortedFunction of I; ::_thesis: ( ( I <> {} & ( for i being set st i in I holds
ex U0 being MSAlgebra over S st
( U0 = A . i & f . i = the Charact of U0 ) ) & ( for i being set st i in I holds
ex U0 being MSAlgebra over S st
( U0 = A . i & g . i = the Charact of U0 ) ) implies f = g ) & ( not I <> {} & f = {} & g = {} implies f = g ) )
hereby ::_thesis: ( not I <> {} & f = {} & g = {} implies f = g )
assume I <> {} ; ::_thesis: ( ( for i being set st i in I holds
ex U0 being MSAlgebra over S st
( U0 = A . i & f . i = the Charact of U0 ) ) & ( for i being set st i in I holds
ex U0 being MSAlgebra over S st
( U0 = A . i & g . i = the Charact of U0 ) ) implies f = g )
assume A3: ( ( for i being set st i in I holds
ex U0 being MSAlgebra over S st
( U0 = A . i & f . i = the Charact of U0 ) ) & ( for i being set st i in I holds
ex U0 being MSAlgebra over S st
( U0 = A . i & g . i = the Charact of U0 ) ) ) ; ::_thesis: f = g
for x being set st x in I holds
f . x = g . x
proof
let x be set ; ::_thesis: ( x in I implies f . x = g . x )
assume A4: x in I ; ::_thesis: f . x = g . x
then reconsider i = x as Element of I ;
( ex U0 being MSAlgebra over S st
( U0 = A . i & f . i = the Charact of U0 ) & ex U0 being MSAlgebra over S st
( U0 = A . i & g . i = the Charact of U0 ) ) by A3, A4;
hence f . x = g . x ; ::_thesis: verum
end;
hence f = g by PBOOLE:3; ::_thesis: verum
end;
thus ( not I <> {} & f = {} & g = {} implies f = g ) ; ::_thesis: verum
end;
correctness
consistency
for b1 being ManySortedFunction of I holds verum;
;
end;
:: deftheorem Def11 defines OPER PRALG_2:def_11_:_
for I being set
for S being non empty ManySortedSign
for A being MSAlgebra-Family of I,S
for b4 being ManySortedFunction of I holds
( ( I <> {} implies ( b4 = OPER A iff for i being set st i in I holds
ex U0 being MSAlgebra over S st
( U0 = A . i & b4 . i = the Charact of U0 ) ) ) & ( not I <> {} implies ( b4 = OPER A iff b4 = {} ) ) );
theorem Th5: :: PRALG_2:5
for I being set
for S being non empty ManySortedSign
for A being MSAlgebra-Family of I,S holds dom (uncurry (OPER A)) = [:I, the carrier' of S:]
proof
let I be set ; ::_thesis: for S being non empty ManySortedSign
for A being MSAlgebra-Family of I,S holds dom (uncurry (OPER A)) = [:I, the carrier' of S:]
let S be non empty ManySortedSign ; ::_thesis: for A being MSAlgebra-Family of I,S holds dom (uncurry (OPER A)) = [:I, the carrier' of S:]
let A be MSAlgebra-Family of I,S; ::_thesis: dom (uncurry (OPER A)) = [:I, the carrier' of S:]
percases ( I <> {} or I = {} ) ;
supposeA1: I <> {} ; ::_thesis: dom (uncurry (OPER A)) = [:I, the carrier' of S:]
thus dom (uncurry (OPER A)) c= [:I, the carrier' of S:] :: according to XBOOLE_0:def_10 ::_thesis: [:I, the carrier' of S:] c= dom (uncurry (OPER A))
proof
let t be set ; :: according to TARSKI:def_3 ::_thesis: ( not t in dom (uncurry (OPER A)) or t in [:I, the carrier' of S:] )
assume t in dom (uncurry (OPER A)) ; ::_thesis: t in [:I, the carrier' of S:]
then consider x being set , g being Function, y being set such that
A2: t = [x,y] and
A3: x in dom (OPER A) and
A4: ( g = (OPER A) . x & y in dom g ) by FUNCT_5:def_2;
reconsider x = x as Element of I by A3, PARTFUN1:def_2;
ex U0 being MSAlgebra over S st
( U0 = A . x & (OPER A) . x = the Charact of U0 ) by A1, Def11;
then A5: y in the carrier' of S by A4, PARTFUN1:def_2;
x in I by A3, PARTFUN1:def_2;
hence t in [:I, the carrier' of S:] by A2, A5, ZFMISC_1:87; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in [:I, the carrier' of S:] or x in dom (uncurry (OPER A)) )
assume A6: x in [:I, the carrier' of S:] ; ::_thesis: x in dom (uncurry (OPER A))
then consider y, z being set such that
A7: x = [y,z] by RELAT_1:def_1;
A8: z in the carrier' of S by A6, A7, ZFMISC_1:87;
reconsider y = y as Element of I by A6, A7, ZFMISC_1:87;
consider U0 being MSAlgebra over S such that
U0 = A . y and
A9: (OPER A) . y = the Charact of U0 by A1, Def11;
( dom the Charact of U0 = the carrier' of S & dom (OPER A) = I ) by PARTFUN1:def_2;
hence x in dom (uncurry (OPER A)) by A1, A7, A8, A9, FUNCT_5:def_2; ::_thesis: verum
end;
supposeA10: I = {} ; ::_thesis: dom (uncurry (OPER A)) = [:I, the carrier' of S:]
then OPER A = {} ;
hence dom (uncurry (OPER A)) = [:I, the carrier' of S:] by A10, FUNCT_5:43, RELAT_1:38, ZFMISC_1:90; ::_thesis: verum
end;
end;
end;
theorem Th6: :: PRALG_2:6
for I being non empty set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S holds commute (OPER A) in Funcs ( the carrier' of S,(Funcs (I,(rng (uncurry (OPER A))))))
proof
let I be non empty set ; ::_thesis: for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S holds commute (OPER A) in Funcs ( the carrier' of S,(Funcs (I,(rng (uncurry (OPER A))))))
let S be non empty non void ManySortedSign ; ::_thesis: for A being MSAlgebra-Family of I,S
for o being OperSymbol of S holds commute (OPER A) in Funcs ( the carrier' of S,(Funcs (I,(rng (uncurry (OPER A))))))
let A be MSAlgebra-Family of I,S; ::_thesis: for o being OperSymbol of S holds commute (OPER A) in Funcs ( the carrier' of S,(Funcs (I,(rng (uncurry (OPER A))))))
let o be OperSymbol of S; ::_thesis: commute (OPER A) in Funcs ( the carrier' of S,(Funcs (I,(rng (uncurry (OPER A))))))
set f = uncurry (OPER A);
dom (uncurry (OPER A)) = [:I, the carrier' of S:] by Th5;
then ( [:I, the carrier' of S:] <> {} & uncurry (OPER A) in Funcs ([:I, the carrier' of S:],(rng (uncurry (OPER A)))) ) by FUNCT_2:def_2, ZFMISC_1:90;
hence commute (OPER A) in Funcs ( the carrier' of S,(Funcs (I,(rng (uncurry (OPER A)))))) by FUNCT_6:10; ::_thesis: verum
end;
definition
let I be set ;
let S be non empty non void ManySortedSign ;
let A be MSAlgebra-Family of I,S;
let o be OperSymbol of S;
funcA ?. o -> ManySortedFunction of I equals :: PRALG_2:def 12
(commute (OPER A)) . o;
coherence
(commute (OPER A)) . o is ManySortedFunction of I
proof
set f = uncurry (OPER A);
set C = commute (OPER A);
A1: dom (uncurry (OPER A)) = [:I, the carrier' of S:] by Th5;
percases ( I <> {} or I = {} ) ;
supposeA2: I <> {} ; ::_thesis: (commute (OPER A)) . o is ManySortedFunction of I
then commute (OPER A) in Funcs ( the carrier' of S,(Funcs (I,(rng (uncurry (OPER A)))))) by Th6;
then A3: ex a being Function st
( a = commute (OPER A) & dom a = the carrier' of S & rng a c= Funcs (I,(rng (uncurry (OPER A)))) ) by FUNCT_2:def_2;
then (commute (OPER A)) . o in rng (commute (OPER A)) by FUNCT_1:def_3;
then consider g being Function such that
A4: g = (commute (OPER A)) . o and
A5: dom g = I and
rng g c= rng (uncurry (OPER A)) by A3, FUNCT_2:def_2;
reconsider g = g as ManySortedSet of I by A5, PARTFUN1:def_2, RELAT_1:def_18;
for x being set st x in dom g holds
g . x is Function
proof
let x be set ; ::_thesis: ( x in dom g implies g . x is Function )
assume x in dom g ; ::_thesis: g . x is Function
then reconsider i = x as Element of I by A5;
A6: ( [i,o] `1 = i & [i,o] `2 = o ) ;
consider U0 being MSAlgebra over S such that
U0 = A . i and
A7: (OPER A) . i = the Charact of U0 by A2, Def11;
A8: [i,o] in dom (uncurry (OPER A)) by A1, A2, ZFMISC_1:87;
then g . i = (uncurry (OPER A)) . (i,o) by A4, FUNCT_5:22;
then g . i = the Charact of U0 . o by A8, A6, A7, FUNCT_5:def_2
.= Den (o,U0) by MSUALG_1:def_6 ;
hence g . x is Function ; ::_thesis: verum
end;
hence (commute (OPER A)) . o is ManySortedFunction of I by A4, FUNCOP_1:def_6; ::_thesis: verum
end;
supposeA9: I = {} ; ::_thesis: (commute (OPER A)) . o is ManySortedFunction of I
reconsider f = [[0]] I as ManySortedFunction of I ;
f = {} by A9
.= (commute {}) . o by FUNCT_6:58
.= (commute (OPER A)) . o by A9 ;
hence (commute (OPER A)) . o is ManySortedFunction of I ; ::_thesis: verum
end;
end;
end;
end;
:: deftheorem defines ?. PRALG_2:def_12_:_
for I being set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S holds A ?. o = (commute (OPER A)) . o;
theorem Th7: :: PRALG_2:7
for I being non empty set
for i being Element of I
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S holds (A ?. o) . i = Den (o,(A . i))
proof
let I be non empty set ; ::_thesis: for i being Element of I
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S holds (A ?. o) . i = Den (o,(A . i))
let i be Element of I; ::_thesis: for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S holds (A ?. o) . i = Den (o,(A . i))
let S be non empty non void ManySortedSign ; ::_thesis: for A being MSAlgebra-Family of I,S
for o being OperSymbol of S holds (A ?. o) . i = Den (o,(A . i))
let A be MSAlgebra-Family of I,S; ::_thesis: for o being OperSymbol of S holds (A ?. o) . i = Den (o,(A . i))
let o be OperSymbol of S; ::_thesis: (A ?. o) . i = Den (o,(A . i))
set O = the carrier' of S;
set f = uncurry (OPER A);
A1: ( [i,o] `1 = i & [i,o] `2 = o ) ;
A2: ex U0 being MSAlgebra over S st
( U0 = A . i & (OPER A) . i = the Charact of U0 ) by Def11;
A3: dom (uncurry (OPER A)) = [:I, the carrier' of S:] by Th5;
then A4: [i,o] in dom (uncurry (OPER A)) by ZFMISC_1:87;
[:I, the carrier' of S:] <> {} by ZFMISC_1:90;
then consider g being Function such that
A5: (curry' (uncurry (OPER A))) . o = g and
dom g = I and
rng g c= rng (uncurry (OPER A)) and
A6: for x being set st x in I holds
g . x = (uncurry (OPER A)) . (x,o) by A3, FUNCT_5:32;
g . i = (uncurry (OPER A)) . (i,o) by A6;
then g . i = the Charact of (A . i) . o by A4, A1, A2, FUNCT_5:def_2
.= Den (o,(A . i)) by MSUALG_1:def_6 ;
hence (A ?. o) . i = Den (o,(A . i)) by A5; ::_thesis: verum
end;
theorem :: PRALG_2:8
for I being non empty set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S
for x being set st x in rng (Frege (A ?. o)) holds
x is Function
proof
let I be non empty set ; ::_thesis: for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S
for x being set st x in rng (Frege (A ?. o)) holds
x is Function
let S be non empty non void ManySortedSign ; ::_thesis: for A being MSAlgebra-Family of I,S
for o being OperSymbol of S
for x being set st x in rng (Frege (A ?. o)) holds
x is Function
let A be MSAlgebra-Family of I,S; ::_thesis: for o being OperSymbol of S
for x being set st x in rng (Frege (A ?. o)) holds
x is Function
let o be OperSymbol of S; ::_thesis: for x being set st x in rng (Frege (A ?. o)) holds
x is Function
let x be set ; ::_thesis: ( x in rng (Frege (A ?. o)) implies x is Function )
assume x in rng (Frege (A ?. o)) ; ::_thesis: x is Function
then ex y being set st
( y in dom (Frege (A ?. o)) & (Frege (A ?. o)) . y = x ) by FUNCT_1:def_3;
hence x is Function ; ::_thesis: verum
end;
theorem Th9: :: PRALG_2:9
for I being non empty set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S
for f being Function st f in rng (Frege (A ?. o)) holds
( dom f = I & ( for i being Element of I holds f . i in Result (o,(A . i)) ) )
proof
let I be non empty set ; ::_thesis: for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S
for f being Function st f in rng (Frege (A ?. o)) holds
( dom f = I & ( for i being Element of I holds f . i in Result (o,(A . i)) ) )
let S be non empty non void ManySortedSign ; ::_thesis: for A being MSAlgebra-Family of I,S
for o being OperSymbol of S
for f being Function st f in rng (Frege (A ?. o)) holds
( dom f = I & ( for i being Element of I holds f . i in Result (o,(A . i)) ) )
let A be MSAlgebra-Family of I,S; ::_thesis: for o being OperSymbol of S
for f being Function st f in rng (Frege (A ?. o)) holds
( dom f = I & ( for i being Element of I holds f . i in Result (o,(A . i)) ) )
let o be OperSymbol of S; ::_thesis: for f being Function st f in rng (Frege (A ?. o)) holds
( dom f = I & ( for i being Element of I holds f . i in Result (o,(A . i)) ) )
let f be Function; ::_thesis: ( f in rng (Frege (A ?. o)) implies ( dom f = I & ( for i being Element of I holds f . i in Result (o,(A . i)) ) ) )
A1: dom (A ?. o) = I by PARTFUN1:def_2;
A2: SubFuncs (rng (A ?. o)) = rng (A ?. o)
proof
thus SubFuncs (rng (A ?. o)) c= rng (A ?. o) by FUNCT_6:18; :: according to XBOOLE_0:def_10 ::_thesis: rng (A ?. o) c= SubFuncs (rng (A ?. o))
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (A ?. o) or x in SubFuncs (rng (A ?. o)) )
assume A3: x in rng (A ?. o) ; ::_thesis: x in SubFuncs (rng (A ?. o))
then ex j being set st
( j in dom (A ?. o) & x = (A ?. o) . j ) by FUNCT_1:def_3;
hence x in SubFuncs (rng (A ?. o)) by A3, FUNCT_6:def_1; ::_thesis: verum
end;
assume f in rng (Frege (A ?. o)) ; ::_thesis: ( dom f = I & ( for i being Element of I holds f . i in Result (o,(A . i)) ) )
then consider y being set such that
A4: y in dom (Frege (A ?. o)) and
A5: (Frege (A ?. o)) . y = f by FUNCT_1:def_3;
A6: dom (Frege (A ?. o)) = product (doms (A ?. o)) by PARTFUN1:def_2;
then consider g being Function such that
A7: g = y and
dom g = dom (doms (A ?. o)) and
A8: for i being set st i in dom (doms (A ?. o)) holds
g . i in (doms (A ?. o)) . i by A4, CARD_3:def_5;
A9: f = (A ?. o) .. g by A4, A5, A6, A7, Def2;
hence dom f = dom (A ?. o) by PRALG_1:def_17
.= I by PARTFUN1:def_2 ;
::_thesis: for i being Element of I holds f . i in Result (o,(A . i))
let i be Element of I; ::_thesis: f . i in Result (o,(A . i))
A10: (A ?. o) . i = Den (o,(A . i)) by Th7;
dom (doms (A ?. o)) = (A ?. o) " (SubFuncs (rng (A ?. o))) by FUNCT_6:def_2
.= dom (A ?. o) by A2, RELAT_1:134 ;
then g . i in (doms (A ?. o)) . i by A8, A1;
then A11: g . i in dom (Den (o,(A . i))) by A1, A10, FUNCT_6:22;
f . i = (Den (o,(A . i))) . (g . i) by A9, A1, A10, PRALG_1:def_17;
then A12: f . i in rng (Den (o,(A . i))) by A11, FUNCT_1:def_3;
rng (Den (o,(A . i))) c= Result (o,(A . i)) by RELAT_1:def_19;
hence f . i in Result (o,(A . i)) by A12; ::_thesis: verum
end;
theorem Th10: :: PRALG_2:10
for I being non empty set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S
for f being Function st f in dom (Frege (A ?. o)) holds
( dom f = I & ( for i being Element of I holds f . i in Args (o,(A . i)) ) & rng f c= Funcs ((dom (the_arity_of o)),|.A.|) )
proof
let I be non empty set ; ::_thesis: for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S
for f being Function st f in dom (Frege (A ?. o)) holds
( dom f = I & ( for i being Element of I holds f . i in Args (o,(A . i)) ) & rng f c= Funcs ((dom (the_arity_of o)),|.A.|) )
let S be non empty non void ManySortedSign ; ::_thesis: for A being MSAlgebra-Family of I,S
for o being OperSymbol of S
for f being Function st f in dom (Frege (A ?. o)) holds
( dom f = I & ( for i being Element of I holds f . i in Args (o,(A . i)) ) & rng f c= Funcs ((dom (the_arity_of o)),|.A.|) )
let A be MSAlgebra-Family of I,S; ::_thesis: for o being OperSymbol of S
for f being Function st f in dom (Frege (A ?. o)) holds
( dom f = I & ( for i being Element of I holds f . i in Args (o,(A . i)) ) & rng f c= Funcs ((dom (the_arity_of o)),|.A.|) )
let o be OperSymbol of S; ::_thesis: for f being Function st f in dom (Frege (A ?. o)) holds
( dom f = I & ( for i being Element of I holds f . i in Args (o,(A . i)) ) & rng f c= Funcs ((dom (the_arity_of o)),|.A.|) )
let f be Function; ::_thesis: ( f in dom (Frege (A ?. o)) implies ( dom f = I & ( for i being Element of I holds f . i in Args (o,(A . i)) ) & rng f c= Funcs ((dom (the_arity_of o)),|.A.|) ) )
assume A1: f in dom (Frege (A ?. o)) ; ::_thesis: ( dom f = I & ( for i being Element of I holds f . i in Args (o,(A . i)) ) & rng f c= Funcs ((dom (the_arity_of o)),|.A.|) )
A2: dom (A ?. o) = I by PARTFUN1:def_2;
A3: SubFuncs (rng (A ?. o)) = rng (A ?. o)
proof
thus SubFuncs (rng (A ?. o)) c= rng (A ?. o) by FUNCT_6:18; :: according to XBOOLE_0:def_10 ::_thesis: rng (A ?. o) c= SubFuncs (rng (A ?. o))
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (A ?. o) or x in SubFuncs (rng (A ?. o)) )
assume A4: x in rng (A ?. o) ; ::_thesis: x in SubFuncs (rng (A ?. o))
then ex j being set st
( j in dom (A ?. o) & x = (A ?. o) . j ) by FUNCT_1:def_3;
hence x in SubFuncs (rng (A ?. o)) by A4, FUNCT_6:def_1; ::_thesis: verum
end;
A5: dom (Frege (A ?. o)) = product (doms (A ?. o)) by PARTFUN1:def_2;
A6: dom (doms (A ?. o)) = (A ?. o) " (SubFuncs (rng (A ?. o))) by FUNCT_6:def_2
.= dom (A ?. o) by A3, RELAT_1:134 ;
hence dom f = I by A1, A5, A2, CARD_3:9; ::_thesis: ( ( for i being Element of I holds f . i in Args (o,(A . i)) ) & rng f c= Funcs ((dom (the_arity_of o)),|.A.|) )
thus A7: for i being Element of I holds f . i in Args (o,(A . i)) ::_thesis: rng f c= Funcs ((dom (the_arity_of o)),|.A.|)
proof
let i be Element of I; ::_thesis: f . i in Args (o,(A . i))
( (A ?. o) . i = Den (o,(A . i)) & f . i in (doms (A ?. o)) . i ) by A1, A5, A2, A6, Th7, CARD_3:9;
then f . i in dom (Den (o,(A . i))) by A2, FUNCT_6:22;
hence f . i in Args (o,(A . i)) by FUNCT_2:def_1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in Funcs ((dom (the_arity_of o)),|.A.|) )
assume x in rng f ; ::_thesis: x in Funcs ((dom (the_arity_of o)),|.A.|)
then consider y being set such that
A8: y in dom f and
A9: x = f . y by FUNCT_1:def_3;
reconsider y = y as Element of I by A1, A5, A2, A6, A8, CARD_3:9;
set X = the carrier' of S;
set AS = ( the Sorts of (A . y) #) * the Arity of S;
set Ar = the Arity of S;
set Cr = the carrier of S;
set So = the Sorts of (A . y);
set a = the_arity_of o;
A10: dom the Arity of S = the carrier' of S by FUNCT_2:def_1;
then A11: dom (( the Sorts of (A . y) #) * the Arity of S) = dom the Arity of S by PARTFUN1:def_2;
A12: Args (o,(A . y)) = (( the Sorts of (A . y) #) * the Arity of S) . o by MSUALG_1:def_4
.= ( the Sorts of (A . y) #) . ( the Arity of S . o) by A10, A11, FUNCT_1:12
.= ( the Sorts of (A . y) #) . (the_arity_of o) by MSUALG_1:def_1
.= product ( the Sorts of (A . y) * (the_arity_of o)) by FINSEQ_2:def_5 ;
x in Args (o,(A . y)) by A7, A9;
then consider g being Function such that
A13: g = x and
A14: dom g = dom ( the Sorts of (A . y) * (the_arity_of o)) and
A15: for i being set st i in dom ( the Sorts of (A . y) * (the_arity_of o)) holds
g . i in ( the Sorts of (A . y) * (the_arity_of o)) . i by A12, CARD_3:def_5;
A16: ( rng (the_arity_of o) c= the carrier of S & dom the Sorts of (A . y) = the carrier of S ) by FINSEQ_1:def_4, PARTFUN1:def_2;
then A17: dom ( the Sorts of (A . y) * (the_arity_of o)) = dom (the_arity_of o) by RELAT_1:27;
A18: rng g c= |.(A . y).|
proof
let i be set ; :: according to TARSKI:def_3 ::_thesis: ( not i in rng g or i in |.(A . y).| )
assume i in rng g ; ::_thesis: i in |.(A . y).|
then consider j being set such that
A19: j in dom g and
A20: g . j = i by FUNCT_1:def_3;
(the_arity_of o) . j in rng (the_arity_of o) by A14, A17, A19, FUNCT_1:def_3;
then A21: the Sorts of (A . y) . ((the_arity_of o) . j) in rng the Sorts of (A . y) by A16, FUNCT_1:def_3;
i in ( the Sorts of (A . y) * (the_arity_of o)) . j by A14, A15, A19, A20;
then i in the Sorts of (A . y) . ((the_arity_of o) . j) by A14, A19, FUNCT_1:12;
hence i in |.(A . y).| by A21, TARSKI:def_4; ::_thesis: verum
end;
|.(A . y).| in { |.(A . i).| where i is Element of I : verum } ;
then |.(A . y).| c= union { |.(A . i).| where i is Element of I : verum } by ZFMISC_1:74;
then rng g c= |.A.| by A18, XBOOLE_1:1;
hence x in Funcs ((dom (the_arity_of o)),|.A.|) by A13, A14, A17, FUNCT_2:def_2; ::_thesis: verum
end;
theorem Th11: :: PRALG_2:11
for I being non empty set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S holds
( dom (doms (A ?. o)) = I & ( for i being Element of I holds (doms (A ?. o)) . i = Args (o,(A . i)) ) )
proof
let I be non empty set ; ::_thesis: for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S holds
( dom (doms (A ?. o)) = I & ( for i being Element of I holds (doms (A ?. o)) . i = Args (o,(A . i)) ) )
let S be non empty non void ManySortedSign ; ::_thesis: for A being MSAlgebra-Family of I,S
for o being OperSymbol of S holds
( dom (doms (A ?. o)) = I & ( for i being Element of I holds (doms (A ?. o)) . i = Args (o,(A . i)) ) )
let A be MSAlgebra-Family of I,S; ::_thesis: for o being OperSymbol of S holds
( dom (doms (A ?. o)) = I & ( for i being Element of I holds (doms (A ?. o)) . i = Args (o,(A . i)) ) )
let o be OperSymbol of S; ::_thesis: ( dom (doms (A ?. o)) = I & ( for i being Element of I holds (doms (A ?. o)) . i = Args (o,(A . i)) ) )
SubFuncs (rng (A ?. o)) = rng (A ?. o)
proof
thus SubFuncs (rng (A ?. o)) c= rng (A ?. o) by FUNCT_6:18; :: according to XBOOLE_0:def_10 ::_thesis: rng (A ?. o) c= SubFuncs (rng (A ?. o))
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (A ?. o) or x in SubFuncs (rng (A ?. o)) )
assume A1: x in rng (A ?. o) ; ::_thesis: x in SubFuncs (rng (A ?. o))
then ex j being set st
( j in dom (A ?. o) & x = (A ?. o) . j ) by FUNCT_1:def_3;
hence x in SubFuncs (rng (A ?. o)) by A1, FUNCT_6:def_1; ::_thesis: verum
end;
then A2: (A ?. o) " (SubFuncs (rng (A ?. o))) = dom (A ?. o) by RELAT_1:134
.= I by PARTFUN1:def_2 ;
A3: dom (A ?. o) = I by PARTFUN1:def_2;
for i being Element of I holds (doms (A ?. o)) . i = Args (o,(A . i))
proof
let i be Element of I; ::_thesis: (doms (A ?. o)) . i = Args (o,(A . i))
(A ?. o) . i = Den (o,(A . i)) by Th7;
then (doms (A ?. o)) . i = dom (Den (o,(A . i))) by A3, FUNCT_6:22;
hence (doms (A ?. o)) . i = Args (o,(A . i)) by FUNCT_2:def_1; ::_thesis: verum
end;
hence ( dom (doms (A ?. o)) = I & ( for i being Element of I holds (doms (A ?. o)) . i = Args (o,(A . i)) ) ) by A2, FUNCT_6:def_2; ::_thesis: verum
end;
definition
let I be set ;
let S be non empty non void ManySortedSign ;
let A be MSAlgebra-Family of I,S;
func OPS A -> ManySortedFunction of ((SORTS A) #) * the Arity of S,(SORTS A) * the ResultSort of S means :: PRALG_2:def 13
for o being OperSymbol of S holds it . o = IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o)))) if I <> {}
otherwise verum;
existence
( ( I <> {} implies ex b1 being ManySortedFunction of ((SORTS A) #) * the Arity of S,(SORTS A) * the ResultSort of S st
for o being OperSymbol of S holds b1 . o = IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o)))) ) & ( not I <> {} implies ex b1 being ManySortedFunction of ((SORTS A) #) * the Arity of S,(SORTS A) * the ResultSort of S st verum ) )
proof
defpred S1[ set , set ] means for o being OperSymbol of S st $1 = o holds
$2 = IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o))));
set X = the carrier' of S;
set AS = ((SORTS A) #) * the Arity of S;
set RS = (SORTS A) * the ResultSort of S;
A1: for x being set st x in the carrier' of S holds
ex y being set st S1[x,y]
proof
let x be set ; ::_thesis: ( x in the carrier' of S implies ex y being set st S1[x,y] )
assume x in the carrier' of S ; ::_thesis: ex y being set st S1[x,y]
then reconsider o = x as OperSymbol of S ;
take IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o)))) ; ::_thesis: S1[x, IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o))))]
let o1 be OperSymbol of S; ::_thesis: ( x = o1 implies IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o)))) = IFEQ ((the_arity_of o1),{},(commute (A ?. o1)),(Commute (Frege (A ?. o1)))) )
assume x = o1 ; ::_thesis: IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o)))) = IFEQ ((the_arity_of o1),{},(commute (A ?. o1)),(Commute (Frege (A ?. o1))))
hence IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o)))) = IFEQ ((the_arity_of o1),{},(commute (A ?. o1)),(Commute (Frege (A ?. o1)))) ; ::_thesis: verum
end;
consider f being Function such that
A2: ( dom f = the carrier' of S & ( for x being set st x in the carrier' of S holds
S1[x,f . x] ) ) from CLASSES1:sch_1(A1);
reconsider f = f as ManySortedSet of the carrier' of S by A2, PARTFUN1:def_2, RELAT_1:def_18;
for x being set st x in dom f holds
f . x is Function
proof
let x be set ; ::_thesis: ( x in dom f implies f . x is Function )
assume x in dom f ; ::_thesis: f . x is Function
then reconsider o = x as OperSymbol of S by A2;
percases ( the_arity_of o = {} or the_arity_of o <> {} ) ;
supposeA3: the_arity_of o = {} ; ::_thesis: f . x is Function
f . x = IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o)))) by A2
.= commute (A ?. o) by A3, FUNCOP_1:def_8 ;
hence f . x is Function ; ::_thesis: verum
end;
supposeA4: the_arity_of o <> {} ; ::_thesis: f . x is Function
f . x = IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o)))) by A2
.= Commute (Frege (A ?. o)) by A4, FUNCOP_1:def_8 ;
hence f . x is Function ; ::_thesis: verum
end;
end;
end;
then reconsider f = f as ManySortedFunction of the carrier' of S by FUNCOP_1:def_6;
hereby ::_thesis: ( not I <> {} implies ex b1 being ManySortedFunction of ((SORTS A) #) * the Arity of S,(SORTS A) * the ResultSort of S st verum )
assume I <> {} ; ::_thesis: ex f being ManySortedFunction of ((SORTS A) #) * the Arity of S,(SORTS A) * the ResultSort of S st
for o being OperSymbol of S holds f . o = IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o))))
then reconsider I9 = I as non empty set ;
reconsider A9 = A as MSAlgebra-Family of I9,S ;
for x being set st x in the carrier' of S holds
f . x is Function of ((((SORTS A) #) * the Arity of S) . x),(((SORTS A) * the ResultSort of S) . x)
proof
let x be set ; ::_thesis: ( x in the carrier' of S implies f . x is Function of ((((SORTS A) #) * the Arity of S) . x),(((SORTS A) * the ResultSort of S) . x) )
assume x in the carrier' of S ; ::_thesis: f . x is Function of ((((SORTS A) #) * the Arity of S) . x),(((SORTS A) * the ResultSort of S) . x)
then reconsider o = x as OperSymbol of S ;
set ar = the_arity_of o;
set C = Commute (Frege (A ?. o));
set F = Frege (A ?. o);
set Ar = the Arity of S;
set Rs = the ResultSort of S;
set Cr = the carrier of S;
set co = commute (A ?. o);
A5: rng (the_arity_of o) c= the carrier of S by FINSEQ_1:def_4;
A6: dom the Arity of S = the carrier' of S by FUNCT_2:def_1;
then dom (((SORTS A) #) * the Arity of S) = dom the Arity of S by PARTFUN1:def_2;
then A7: (((SORTS A) #) * the Arity of S) . o = ((SORTS A) #) . ( the Arity of S . o) by A6, FUNCT_1:12
.= ((SORTS A) #) . (the_arity_of o) by MSUALG_1:def_1
.= product ((SORTS A) * (the_arity_of o)) by FINSEQ_2:def_5 ;
A8: dom the ResultSort of S = the carrier' of S by FUNCT_2:def_1;
then dom ((SORTS A) * the ResultSort of S) = dom the ResultSort of S by PARTFUN1:def_2;
then A9: ((SORTS A) * the ResultSort of S) . o = (SORTS A) . ( the ResultSort of S . o) by A8, FUNCT_1:12
.= (SORTS A) . (the_result_sort_of o) by MSUALG_1:def_2
.= product (Carrier (A,(the_result_sort_of o))) by Def10 ;
dom (SORTS A) = the carrier of S by PARTFUN1:def_2;
then A10: dom ((SORTS A) * (the_arity_of o)) = dom (the_arity_of o) by A5, RELAT_1:27;
percases ( the_arity_of o = {} or the_arity_of o <> {} ) ;
supposeA11: the_arity_of o = {} ; ::_thesis: f . x is Function of ((((SORTS A) #) * the Arity of S) . x),(((SORTS A) * the ResultSort of S) . x)
set rs = the_result_sort_of o;
A12: rng (A ?. o) c= Funcs ({{}},|.A9.|)
proof
let j be set ; :: according to TARSKI:def_3 ::_thesis: ( not j in rng (A ?. o) or j in Funcs ({{}},|.A9.|) )
assume j in rng (A ?. o) ; ::_thesis: j in Funcs ({{}},|.A9.|)
then consider a being set such that
A13: a in dom (A ?. o) and
A14: (A ?. o) . a = j by FUNCT_1:def_3;
reconsider i = a as Element of I9 by A13, PARTFUN1:def_2;
set So = the Sorts of (A9 . i);
|.(A9 . i).| in { |.(A9 . d).| where d is Element of I9 : verum } ;
then A15: |.(A9 . i).| c= union { |.(A9 . d).| where d is Element of I9 : verum } by ZFMISC_1:74;
dom the Sorts of (A9 . i) = the carrier of S by PARTFUN1:def_2;
then the Sorts of (A9 . i) . (the_result_sort_of o) in rng the Sorts of (A9 . i) by FUNCT_1:def_3;
then A16: the Sorts of (A9 . i) . (the_result_sort_of o) c= union (rng the Sorts of (A9 . i)) by ZFMISC_1:74;
( rng (Den (o,(A9 . i))) c= Result (o,(A9 . i)) & Result (o,(A9 . i)) = the Sorts of (A9 . i) . (the_result_sort_of o) ) by Th3, RELAT_1:def_19;
then rng (Den (o,(A9 . i))) c= |.(A9 . i).| by A16, XBOOLE_1:1;
then A17: rng (Den (o,(A9 . i))) c= |.A9.| by A15, XBOOLE_1:1;
A18: ( dom (Den (o,(A9 . i))) = Args (o,(A9 . i)) & Args (o,(A9 . i)) = {{}} ) by A11, Th4, FUNCT_2:def_1;
j = Den (o,(A9 . i)) by A14, Th7;
hence j in Funcs ({{}},|.A9.|) by A18, A17, FUNCT_2:def_2; ::_thesis: verum
end;
dom (A ?. o) = I by PARTFUN1:def_2;
then A19: A ?. o in Funcs (I,(Funcs ({{}},|.A9.|))) by A12, FUNCT_2:def_2;
then commute (A ?. o) in Funcs ({{}},(Funcs (I,|.A9.|))) by FUNCT_6:55;
then A20: ex h being Function st
( h = commute (A ?. o) & dom h = {{}} & rng h c= Funcs (I,|.A9.|) ) by FUNCT_2:def_2;
A21: rng (commute (A ?. o)) c= ((SORTS A) * the ResultSort of S) . o
proof
let j be set ; :: according to TARSKI:def_3 ::_thesis: ( not j in rng (commute (A ?. o)) or j in ((SORTS A) * the ResultSort of S) . o )
A22: dom (Carrier (A,(the_result_sort_of o))) = I by PARTFUN1:def_2;
assume A23: j in rng (commute (A ?. o)) ; ::_thesis: j in ((SORTS A) * the ResultSort of S) . o
then consider a being set such that
A24: a in dom (commute (A ?. o)) and
A25: (commute (A ?. o)) . a = j by FUNCT_1:def_3;
reconsider h = j as Function by A25;
A26: for b being set st b in dom (Carrier (A,(the_result_sort_of o))) holds
h . b in (Carrier (A,(the_result_sort_of o))) . b
proof
let b be set ; ::_thesis: ( b in dom (Carrier (A,(the_result_sort_of o))) implies h . b in (Carrier (A,(the_result_sort_of o))) . b )
assume b in dom (Carrier (A,(the_result_sort_of o))) ; ::_thesis: h . b in (Carrier (A,(the_result_sort_of o))) . b
then reconsider i = b as Element of I9 by PARTFUN1:def_2;
A27: ex U0 being MSAlgebra over S st
( U0 = A . i & (Carrier (A,(the_result_sort_of o))) . i = the Sorts of U0 . (the_result_sort_of o) ) by Def9;
dom (Den (o,(A9 . i))) = Args (o,(A9 . i)) by FUNCT_2:def_1
.= {{}} by A11, Th4 ;
then A28: (Den (o,(A9 . i))) . a in rng (Den (o,(A9 . i))) by A20, A24, FUNCT_1:def_3;
(A ?. o) . i = Den (o,(A9 . i)) by Th7;
then A29: (Den (o,(A9 . i))) . a = h . i by A19, A20, A24, A25, FUNCT_6:56;
rng (Den (o,(A9 . i))) c= Result (o,(A9 . i)) by RELAT_1:def_19;
then h . i in Result (o,(A9 . i)) by A29, A28;
hence h . b in (Carrier (A,(the_result_sort_of o))) . b by A27, Th3; ::_thesis: verum
end;
ex k being Function st
( k = h & dom k = I & rng k c= |.A9.| ) by A20, A23, FUNCT_2:def_2;
hence j in ((SORTS A) * the ResultSort of S) . o by A9, A22, A26, CARD_3:9; ::_thesis: verum
end;
A30: (((SORTS A) #) * the Arity of S) . o = {{}} by A7, A11, CARD_3:10;
f . x = IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o)))) by A2
.= commute (A ?. o) by A11, FUNCOP_1:def_8 ;
hence f . x is Function of ((((SORTS A) #) * the Arity of S) . x),(((SORTS A) * the ResultSort of S) . x) by A30, A20, A21, FUNCT_2:2; ::_thesis: verum
end;
supposeA31: the_arity_of o <> {} ; ::_thesis: f . x is Function of ((((SORTS A) #) * the Arity of S) . x),(((SORTS A) * the ResultSort of S) . x)
A32: dom (Commute (Frege (A ?. o))) = (((SORTS A) #) * the Arity of S) . o
proof
thus dom (Commute (Frege (A ?. o))) c= (((SORTS A) #) * the Arity of S) . o :: according to XBOOLE_0:def_10 ::_thesis: (((SORTS A) #) * the Arity of S) . o c= dom (Commute (Frege (A ?. o)))
proof
let j be set ; :: according to TARSKI:def_3 ::_thesis: ( not j in dom (Commute (Frege (A ?. o))) or j in (((SORTS A) #) * the Arity of S) . o )
assume j in dom (Commute (Frege (A ?. o))) ; ::_thesis: j in (((SORTS A) #) * the Arity of S) . o
then consider g being Function such that
A33: g in dom (Frege (A ?. o)) and
A34: j = commute g by Def1;
set cg = commute g;
A35: rng g c= Funcs ((dom (the_arity_of o)),|.A9.|) by A33, Th10;
A36: dom g = I9 by A33, Th10;
then A37: g in Funcs (I,(Funcs ((dom (the_arity_of o)),|.A9.|))) by A35, FUNCT_2:def_2;
then commute g in Funcs ((dom (the_arity_of o)),(Funcs (I,|.A9.|))) by A31, FUNCT_6:55;
then A38: ex h being Function st
( h = commute g & dom h = dom (the_arity_of o) & rng h c= Funcs (I,|.A9.|) ) by FUNCT_2:def_2;
for y being set st y in dom ((SORTS A) * (the_arity_of o)) holds
(commute g) . y in ((SORTS A) * (the_arity_of o)) . y
proof
let y be set ; ::_thesis: ( y in dom ((SORTS A) * (the_arity_of o)) implies (commute g) . y in ((SORTS A) * (the_arity_of o)) . y )
assume A39: y in dom ((SORTS A) * (the_arity_of o)) ; ::_thesis: (commute g) . y in ((SORTS A) * (the_arity_of o)) . y
then (the_arity_of o) . y in rng (the_arity_of o) by A10, FUNCT_1:def_3;
then reconsider s = (the_arity_of o) . y as SortSymbol of S by A5;
(commute g) . y in rng (commute g) by A10, A38, A39, FUNCT_1:def_3;
then consider h being Function such that
A40: h = (commute g) . y and
A41: dom h = I and
rng h c= |.A9.| by A38, FUNCT_2:def_2;
A42: for z being set st z in dom (Carrier (A,s)) holds
h . z in (Carrier (A,s)) . z
proof
let z be set ; ::_thesis: ( z in dom (Carrier (A,s)) implies h . z in (Carrier (A,s)) . z )
assume z in dom (Carrier (A,s)) ; ::_thesis: h . z in (Carrier (A,s)) . z
then reconsider i = z as Element of I9 by PARTFUN1:def_2;
A43: dom (( the Sorts of (A9 . i) #) * the Arity of S) = the carrier' of S by PARTFUN1:def_2;
A44: Args (o,(A9 . i)) = (( the Sorts of (A9 . i) #) * the Arity of S) . o by MSUALG_1:def_4
.= ( the Sorts of (A9 . i) #) . ( the Arity of S . o) by A43, FUNCT_1:12
.= ( the Sorts of (A9 . i) #) . (the_arity_of o) by MSUALG_1:def_1
.= product ( the Sorts of (A9 . i) * (the_arity_of o)) by FINSEQ_2:def_5 ;
g . i in rng g by A36, FUNCT_1:def_3;
then consider f being Function such that
A45: f = g . i and
dom f = dom (the_arity_of o) and
rng f c= |.A9.| by A35, FUNCT_2:def_2;
A46: ex U0 being MSAlgebra over S st
( U0 = A . i & (Carrier (A,s)) . i = the Sorts of U0 . s ) by Def9;
dom the Sorts of (A9 . i) = the carrier of S by PARTFUN1:def_2;
then A47: dom ( the Sorts of (A9 . i) * (the_arity_of o)) = dom (the_arity_of o) by A5, RELAT_1:27;
then A48: ( the Sorts of (A9 . i) * (the_arity_of o)) . y = the Sorts of (A9 . i) . s by A10, A39, FUNCT_1:12;
g . i in Args (o,(A9 . i)) by A33, Th10;
then f . y in ( the Sorts of (A9 . i) * (the_arity_of o)) . y by A10, A39, A45, A44, A47, CARD_3:9;
hence h . z in (Carrier (A,s)) . z by A10, A37, A39, A40, A46, A45, A48, FUNCT_6:56; ::_thesis: verum
end;
A49: dom (Carrier (A,s)) = I by PARTFUN1:def_2;
((SORTS A) * (the_arity_of o)) . y = (SORTS A) . s by A39, FUNCT_1:12
.= product (Carrier (A,s)) by Def10 ;
hence (commute g) . y in ((SORTS A) * (the_arity_of o)) . y by A49, A40, A41, A42, CARD_3:9; ::_thesis: verum
end;
hence j in (((SORTS A) #) * the Arity of S) . o by A7, A10, A34, A38, CARD_3:9; ::_thesis: verum
end;
let i be set ; :: according to TARSKI:def_3 ::_thesis: ( not i in (((SORTS A) #) * the Arity of S) . o or i in dom (Commute (Frege (A ?. o))) )
assume i in (((SORTS A) #) * the Arity of S) . o ; ::_thesis: i in dom (Commute (Frege (A ?. o)))
then consider g being Function such that
A50: g = i and
A51: dom g = dom ((SORTS A) * (the_arity_of o)) and
A52: for x being set st x in dom ((SORTS A) * (the_arity_of o)) holds
g . x in ((SORTS A) * (the_arity_of o)) . x by A7, CARD_3:def_5;
A53: rng g c= Funcs (I,|.A9.|)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in rng g or a in Funcs (I,|.A9.|) )
assume a in rng g ; ::_thesis: a in Funcs (I,|.A9.|)
then consider b being set such that
A54: b in dom g and
A55: g . b = a by FUNCT_1:def_3;
(the_arity_of o) . b in rng (the_arity_of o) by A10, A51, A54, FUNCT_1:def_3;
then reconsider cr = (the_arity_of o) . b as SortSymbol of S by A5;
A56: ((SORTS A) * (the_arity_of o)) . b = (SORTS A) . cr by A51, A54, FUNCT_1:12
.= product (Carrier (A,cr)) by Def10 ;
a in ((SORTS A) * (the_arity_of o)) . b by A51, A52, A54, A55;
then consider h being Function such that
A57: h = a and
A58: dom h = dom (Carrier (A,cr)) and
A59: for j being set st j in dom (Carrier (A,cr)) holds
h . j in (Carrier (A,cr)) . j by A56, CARD_3:def_5;
A60: rng h c= |.A9.|
proof
let j be set ; :: according to TARSKI:def_3 ::_thesis: ( not j in rng h or j in |.A9.| )
assume j in rng h ; ::_thesis: j in |.A9.|
then consider c being set such that
A61: c in dom h and
A62: h . c = j by FUNCT_1:def_3;
reconsider i = c as Element of I9 by A58, A61, PARTFUN1:def_2;
( ex U0 being MSAlgebra over S st
( U0 = A . i & (Carrier (A,cr)) . i = the Sorts of U0 . cr ) & dom the Sorts of (A9 . i) = the carrier of S ) by Def9, PARTFUN1:def_2;
then A63: (Carrier (A,cr)) . i in rng the Sorts of (A9 . i) by FUNCT_1:def_3;
h . i in (Carrier (A,cr)) . i by A58, A59, A61;
then A64: h . i in |.(A9 . i).| by A63, TARSKI:def_4;
|.(A9 . i).| in { |.(A9 . d).| where d is Element of I9 : verum } ;
hence j in |.A9.| by A62, A64, TARSKI:def_4; ::_thesis: verum
end;
dom (Carrier (A,cr)) = I by PARTFUN1:def_2;
hence a in Funcs (I,|.A9.|) by A57, A58, A60, FUNCT_2:def_2; ::_thesis: verum
end;
then A65: g in Funcs ((dom (the_arity_of o)),(Funcs (I,|.A9.|))) by A10, A51, FUNCT_2:def_2;
then A66: commute (commute g) = g by A31, FUNCT_6:57;
commute g in Funcs (I,(Funcs ((dom (the_arity_of o)),|.A9.|))) by A31, A65, FUNCT_6:55;
then A67: ex h being Function st
( h = commute g & dom h = I & rng h c= Funcs ((dom (the_arity_of o)),|.A9.|) ) by FUNCT_2:def_2;
A68: for j being set st j in dom (doms (A ?. o)) holds
(commute g) . j in (doms (A ?. o)) . j
proof
set cg = commute g;
let j be set ; ::_thesis: ( j in dom (doms (A ?. o)) implies (commute g) . j in (doms (A ?. o)) . j )
assume j in dom (doms (A ?. o)) ; ::_thesis: (commute g) . j in (doms (A ?. o)) . j
then reconsider ii = j as Element of I9 by Th11;
set So = the Sorts of (A9 . ii);
reconsider h = (commute g) . ii as Function ;
h in rng (commute g) by A67, FUNCT_1:def_3;
then A69: ex s being Function st
( s = h & dom s = dom (the_arity_of o) & rng s c= |.A9.| ) by A67, FUNCT_2:def_2;
A70: dom ( the Sorts of (A9 . ii) * (the_arity_of o)) = dom (the_arity_of o) by Th3;
A71: for a being set st a in dom ( the Sorts of (A9 . ii) * (the_arity_of o)) holds
h . a in ( the Sorts of (A9 . ii) * (the_arity_of o)) . a
proof
let a be set ; ::_thesis: ( a in dom ( the Sorts of (A9 . ii) * (the_arity_of o)) implies h . a in ( the Sorts of (A9 . ii) * (the_arity_of o)) . a )
assume A72: a in dom ( the Sorts of (A9 . ii) * (the_arity_of o)) ; ::_thesis: h . a in ( the Sorts of (A9 . ii) * (the_arity_of o)) . a
then (the_arity_of o) . a in rng (the_arity_of o) by A70, FUNCT_1:def_3;
then reconsider s = (the_arity_of o) . a as SortSymbol of S by A5;
A73: ( the Sorts of (A9 . ii) * (the_arity_of o)) . a = the Sorts of (A9 . ii) . s by A72, FUNCT_1:12;
g . a in rng g by A10, A51, A70, A72, FUNCT_1:def_3;
then consider k being Function such that
A74: k = g . a and
dom k = I and
rng k c= |.A9.| by A53, FUNCT_2:def_2;
A75: ( ex U0 being MSAlgebra over S st
( U0 = A9 . ii & (Carrier (A,s)) . ii = the Sorts of U0 . s ) & dom (Carrier (A,s)) = I ) by Def9, PARTFUN1:def_2;
A76: ((SORTS A) * (the_arity_of o)) . a = (SORTS A) . s by A10, A70, A72, FUNCT_1:12
.= product (Carrier (A,s)) by Def10 ;
( k . ii = h . a & k in ((SORTS A) * (the_arity_of o)) . a ) by A10, A52, A65, A70, A72, A74, FUNCT_6:56;
hence h . a in ( the Sorts of (A9 . ii) * (the_arity_of o)) . a by A73, A76, A75, CARD_3:9; ::_thesis: verum
end;
( (doms (A ?. o)) . ii = Args (o,(A9 . ii)) & Args (o,(A9 . ii)) = product ( the Sorts of (A9 . ii) * (the_arity_of o)) ) by Th3, Th11;
hence (commute g) . j in (doms (A ?. o)) . j by A70, A69, A71, CARD_3:9; ::_thesis: verum
end;
( dom (Frege (A ?. o)) = product (doms (A ?. o)) & dom (doms (A ?. o)) = I9 ) by Th11, PARTFUN1:def_2;
then commute g in dom (Frege (A ?. o)) by A67, A68, CARD_3:9;
hence i in dom (Commute (Frege (A ?. o))) by A50, A66, Def1; ::_thesis: verum
end;
set rs = the_result_sort_of o;
set CA = Carrier (A,(the_result_sort_of o));
A77: rng (Commute (Frege (A ?. o))) c= ((SORTS A) * the ResultSort of S) . o
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (Commute (Frege (A ?. o))) or x in ((SORTS A) * the ResultSort of S) . o )
A78: dom (Carrier (A,(the_result_sort_of o))) = I by PARTFUN1:def_2;
assume x in rng (Commute (Frege (A ?. o))) ; ::_thesis: x in ((SORTS A) * the ResultSort of S) . o
then consider g being set such that
A79: g in dom (Commute (Frege (A ?. o))) and
A80: (Commute (Frege (A ?. o))) . g = x by FUNCT_1:def_3;
consider f being Function such that
A81: f in dom (Frege (A ?. o)) and
A82: g = commute f by A79, Def1;
reconsider g = g as Function by A82;
( dom f = I9 & rng f c= Funcs ((dom (the_arity_of o)),|.A9.|) ) by A81, Th10;
then f in Funcs (I,(Funcs ((dom (the_arity_of o)),|.A9.|))) by FUNCT_2:def_2;
then commute g = f by A31, A82, FUNCT_6:57;
then A83: x = (Frege (A ?. o)) . f by A79, A80, Def1;
then reconsider h = x as Function ;
A84: (Frege (A ?. o)) . f in rng (Frege (A ?. o)) by A81, FUNCT_1:def_3;
A85: for j being set st j in dom (Carrier (A,(the_result_sort_of o))) holds
h . j in (Carrier (A,(the_result_sort_of o))) . j
proof
let j be set ; ::_thesis: ( j in dom (Carrier (A,(the_result_sort_of o))) implies h . j in (Carrier (A,(the_result_sort_of o))) . j )
assume j in dom (Carrier (A,(the_result_sort_of o))) ; ::_thesis: h . j in (Carrier (A,(the_result_sort_of o))) . j
then reconsider i = j as Element of I9 by PARTFUN1:def_2;
A86: dom ( the Sorts of (A9 . i) * the ResultSort of S) = dom the ResultSort of S by A8, PARTFUN1:def_2;
A87: ex U0 being MSAlgebra over S st
( U0 = A9 . i & (Carrier (A,(the_result_sort_of o))) . i = the Sorts of U0 . (the_result_sort_of o) ) by Def9;
Result (o,(A9 . i)) = ( the Sorts of (A9 . i) * the ResultSort of S) . o by MSUALG_1:def_5
.= the Sorts of (A9 . i) . ( the ResultSort of S . o) by A8, A86, FUNCT_1:12
.= (Carrier (A,(the_result_sort_of o))) . i by A87, MSUALG_1:def_2 ;
hence h . j in (Carrier (A,(the_result_sort_of o))) . j by A83, A84, Th9; ::_thesis: verum
end;
dom h = I9 by A83, A84, Th9;
hence x in ((SORTS A) * the ResultSort of S) . o by A9, A78, A85, CARD_3:9; ::_thesis: verum
end;
f . x = IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o)))) by A2
.= Commute (Frege (A ?. o)) by A31, FUNCOP_1:def_8 ;
hence f . x is Function of ((((SORTS A) #) * the Arity of S) . x),(((SORTS A) * the ResultSort of S) . x) by A32, A77, FUNCT_2:2; ::_thesis: verum
end;
end;
end;
then reconsider f = f as ManySortedFunction of ((SORTS A) #) * the Arity of S,(SORTS A) * the ResultSort of S by PBOOLE:def_15;
take f = f; ::_thesis: for o being OperSymbol of S holds f . o = IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o))))
let o be OperSymbol of S; ::_thesis: f . o = IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o))))
thus f . o = IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o)))) by A2; ::_thesis: verum
end;
assume I = {} ; ::_thesis: ex b1 being ManySortedFunction of ((SORTS A) #) * the Arity of S,(SORTS A) * the ResultSort of S st verum
set f = the ManySortedFunction of ((SORTS A) #) * the Arity of S,(SORTS A) * the ResultSort of S;
take the ManySortedFunction of ((SORTS A) #) * the Arity of S,(SORTS A) * the ResultSort of S ; ::_thesis: verum
end;
uniqueness
for b1, b2 being ManySortedFunction of ((SORTS A) #) * the Arity of S,(SORTS A) * the ResultSort of S holds
( ( I <> {} & ( for o being OperSymbol of S holds b1 . o = IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o)))) ) & ( for o being OperSymbol of S holds b2 . o = IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o)))) ) implies b1 = b2 ) & ( not I <> {} implies b1 = b2 ) )
proof
let f, g be ManySortedFunction of ((SORTS A) #) * the Arity of S,(SORTS A) * the ResultSort of S; ::_thesis: ( ( I <> {} & ( for o being OperSymbol of S holds f . o = IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o)))) ) & ( for o being OperSymbol of S holds g . o = IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o)))) ) implies f = g ) & ( not I <> {} implies f = g ) )
hereby ::_thesis: ( not I <> {} implies f = g )
assume I <> {} ; ::_thesis: ( ( for o being OperSymbol of S holds f . o = IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o)))) ) & ( for o being OperSymbol of S holds g . o = IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o)))) ) implies f = g )
assume that
A88: for o being OperSymbol of S holds f . o = IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o)))) and
A89: for o being OperSymbol of S holds g . o = IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o)))) ; ::_thesis: f = g
for i being set st i in the carrier' of S holds
f . i = g . i
proof
let i be set ; ::_thesis: ( i in the carrier' of S implies f . i = g . i )
assume i in the carrier' of S ; ::_thesis: f . i = g . i
then reconsider o = i as Element of the carrier' of S ;
f . o = IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o)))) by A88;
hence f . i = g . i by A89; ::_thesis: verum
end;
hence f = g by PBOOLE:3; ::_thesis: verum
end;
assume A90: I = {} ; ::_thesis: f = g
A91: now__::_thesis:_for_o_being_set_st_o_in_the_carrier'_of_S_holds_
f_._o_=_g_._o
let o be set ; ::_thesis: ( o in the carrier' of S implies f . o = g . o )
assume A92: o in the carrier' of S ; ::_thesis: f . o = g . o
then reconsider s = the ResultSort of S . o as SortSymbol of S by FUNCT_2:5;
o in dom the ResultSort of S by A92, FUNCT_2:def_1;
then A93: ((SORTS A) * the ResultSort of S) . o = (SORTS A) . s by FUNCT_1:13
.= product (Carrier (A,s)) by Def10
.= {{}} by A90, CARD_3:10 ;
( f . o is Function of ((((SORTS A) #) * the Arity of S) . o),(((SORTS A) * the ResultSort of S) . o) & g . o is Function of ((((SORTS A) #) * the Arity of S) . o),(((SORTS A) * the ResultSort of S) . o) ) by A92, PBOOLE:def_15;
hence f . o = g . o by A93, FUNCT_2:51; ::_thesis: verum
end;
( dom f = the carrier' of S & dom g = the carrier' of S ) by PARTFUN1:def_2;
hence f = g by A91, FUNCT_1:2; ::_thesis: verum
end;
correctness
consistency
for b1 being ManySortedFunction of ((SORTS A) #) * the Arity of S,(SORTS A) * the ResultSort of S holds verum;
;
end;
:: deftheorem defines OPS PRALG_2:def_13_:_
for I being set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for b4 being ManySortedFunction of ((SORTS A) #) * the Arity of S,(SORTS A) * the ResultSort of S holds
( ( I <> {} implies ( b4 = OPS A iff for o being OperSymbol of S holds b4 . o = IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o)))) ) ) & ( not I <> {} implies ( b4 = OPS A iff verum ) ) );
definition
let I be set ;
let S be non empty non void ManySortedSign ;
let A be MSAlgebra-Family of I,S;
func product A -> MSAlgebra over S equals :: PRALG_2:def 14
MSAlgebra(# (SORTS A),(OPS A) #);
coherence
MSAlgebra(# (SORTS A),(OPS A) #) is MSAlgebra over S ;
end;
:: deftheorem defines product PRALG_2:def_14_:_
for I being set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S holds product A = MSAlgebra(# (SORTS A),(OPS A) #);
registration
let I be set ;
let S be non empty non void ManySortedSign ;
let A be MSAlgebra-Family of I,S;
cluster product A -> strict ;
coherence
product A is strict ;
end;
theorem :: PRALG_2:12
for I being set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S holds
( the Sorts of (product A) = SORTS A & the Charact of (product A) = OPS A ) ;