:: PRALG_1 semantic presentation
begin
definition
let A, B be non empty set ;
let h1 be FinSequence of [:A,B:];
:: original: pr1
redefine func pr1 h1 -> FinSequence of A means :Def1: :: PRALG_1:def 1
( len it = len h1 & ( for n being Nat st n in dom it holds
it . n = (h1 . n) `1 ) );
compatibility
for b1 being FinSequence of A holds
( b1 = pr1 h1 iff ( len b1 = len h1 & ( for n being Nat st n in dom b1 holds
b1 . n = (h1 . n) `1 ) ) )
proof
let f1 be FinSequence of A; ::_thesis: ( f1 = pr1 h1 iff ( len f1 = len h1 & ( for n being Nat st n in dom f1 holds
f1 . n = (h1 . n) `1 ) ) )
hereby ::_thesis: ( len f1 = len h1 & ( for n being Nat st n in dom f1 holds
f1 . n = (h1 . n) `1 ) implies f1 = pr1 h1 )
assume A1: f1 = pr1 h1 ; ::_thesis: ( len f1 = len h1 & ( for n being Nat st n in dom f1 holds
f1 . n = (h1 . n) `1 ) )
then A2: dom f1 = dom h1 by MCART_1:def_12;
hence len f1 = len h1 by FINSEQ_3:29; ::_thesis: for n being Nat st n in dom f1 holds
f1 . n = (h1 . n) `1
let n be Nat; ::_thesis: ( n in dom f1 implies f1 . n = (h1 . n) `1 )
thus ( n in dom f1 implies f1 . n = (h1 . n) `1 ) by A1, A2, MCART_1:def_12; ::_thesis: verum
end;
assume ( len f1 = len h1 & ( for n being Nat st n in dom f1 holds
f1 . n = (h1 . n) `1 ) ) ; ::_thesis: f1 = pr1 h1
then ( dom f1 = dom h1 & ( for n being set st n in dom f1 holds
f1 . n = (h1 . n) `1 ) ) by FINSEQ_3:29;
hence f1 = pr1 h1 by MCART_1:def_12; ::_thesis: verum
end;
coherence
pr1 h1 is FinSequence of A
proof
thus pr1 h1 is FinSequence of A ; ::_thesis: verum
end;
:: original: pr2
redefine func pr2 h1 -> FinSequence of B means :Def2: :: PRALG_1:def 2
( len it = len h1 & ( for n being Nat st n in dom it holds
it . n = (h1 . n) `2 ) );
compatibility
for b1 being FinSequence of B holds
( b1 = pr2 h1 iff ( len b1 = len h1 & ( for n being Nat st n in dom b1 holds
b1 . n = (h1 . n) `2 ) ) )
proof
let f1 be FinSequence of B; ::_thesis: ( f1 = pr2 h1 iff ( len f1 = len h1 & ( for n being Nat st n in dom f1 holds
f1 . n = (h1 . n) `2 ) ) )
hereby ::_thesis: ( len f1 = len h1 & ( for n being Nat st n in dom f1 holds
f1 . n = (h1 . n) `2 ) implies f1 = pr2 h1 )
assume A3: f1 = pr2 h1 ; ::_thesis: ( len f1 = len h1 & ( for n being Nat st n in dom f1 holds
f1 . n = (h1 . n) `2 ) )
then A4: dom f1 = dom h1 by MCART_1:def_13;
hence len f1 = len h1 by FINSEQ_3:29; ::_thesis: for n being Nat st n in dom f1 holds
f1 . n = (h1 . n) `2
let n be Nat; ::_thesis: ( n in dom f1 implies f1 . n = (h1 . n) `2 )
thus ( n in dom f1 implies f1 . n = (h1 . n) `2 ) by A3, A4, MCART_1:def_13; ::_thesis: verum
end;
assume ( len f1 = len h1 & ( for n being Nat st n in dom f1 holds
f1 . n = (h1 . n) `2 ) ) ; ::_thesis: f1 = pr2 h1
then ( dom f1 = dom h1 & ( for n being set st n in dom f1 holds
f1 . n = (h1 . n) `2 ) ) by FINSEQ_3:29;
hence f1 = pr2 h1 by MCART_1:def_13; ::_thesis: verum
end;
coherence
pr2 h1 is FinSequence of B
proof
thus pr2 h1 is FinSequence of B ; ::_thesis: verum
end;
end;
:: deftheorem Def1 defines pr1 PRALG_1:def_1_:_
for A, B being non empty set
for h1 being FinSequence of [:A,B:]
for b4 being FinSequence of A holds
( b4 = pr1 h1 iff ( len b4 = len h1 & ( for n being Nat st n in dom b4 holds
b4 . n = (h1 . n) `1 ) ) );
:: deftheorem Def2 defines pr2 PRALG_1:def_2_:_
for A, B being non empty set
for h1 being FinSequence of [:A,B:]
for b4 being FinSequence of B holds
( b4 = pr2 h1 iff ( len b4 = len h1 & ( for n being Nat st n in dom b4 holds
b4 . n = (h1 . n) `2 ) ) );
definition
let A, B be non empty set ;
let f1 be non empty homogeneous quasi_total PartFunc of (A *),A;
let f2 be non empty homogeneous quasi_total PartFunc of (B *),B;
assume A1: arity f1 = arity f2 ;
func[[:f1,f2:]] -> non empty homogeneous quasi_total PartFunc of ([:A,B:] *),[:A,B:] means :Def3: :: PRALG_1:def 3
( dom it = (arity f1) -tuples_on [:A,B:] & ( for h being FinSequence of [:A,B:] st h in dom it holds
it . h = [(f1 . (pr1 h)),(f2 . (pr2 h))] ) );
existence
ex b1 being non empty homogeneous quasi_total PartFunc of ([:A,B:] *),[:A,B:] st
( dom b1 = (arity f1) -tuples_on [:A,B:] & ( for h being FinSequence of [:A,B:] st h in dom b1 holds
b1 . h = [(f1 . (pr1 h)),(f2 . (pr2 h))] ) )
proof
set ar = (arity f1) -tuples_on [:A,B:];
set ab = { s where s is Element of [:A,B:] * : len s = arity f1 } ;
defpred S1[ set , set ] means for h being FinSequence of [:A,B:] st $1 = h holds
$2 = [(f1 . (pr1 h)),(f2 . (pr2 h))];
A2: dom f2 = (arity f2) -tuples_on B by MARGREL1:22;
A3: ( rng f1 c= A & rng f2 c= B ) by RELAT_1:def_19;
A4: dom f1 = (arity f1) -tuples_on A by MARGREL1:22;
A5: for x, y being set st x in (arity f1) -tuples_on [:A,B:] & S1[x,y] holds
y in [:A,B:]
proof
let x, y be set ; ::_thesis: ( x in (arity f1) -tuples_on [:A,B:] & S1[x,y] implies y in [:A,B:] )
assume that
A6: x in (arity f1) -tuples_on [:A,B:] and
A7: S1[x,y] ; ::_thesis: y in [:A,B:]
consider s being Element of [:A,B:] * such that
A8: x = s and
A9: len s = arity f1 by A6;
reconsider s1 = pr1 s as Element of A * by FINSEQ_1:def_11;
len (pr1 s) = len s by Def1;
then s1 in { s3 where s3 is Element of A * : len s3 = arity f1 } by A9;
then A10: f1 . s1 in rng f1 by A4, FUNCT_1:def_3;
reconsider s2 = pr2 s as Element of B * by FINSEQ_1:def_11;
len (pr2 s) = len s by Def2;
then s2 in { s3 where s3 is Element of B * : len s3 = arity f2 } by A1, A9;
then A11: f2 . s2 in rng f2 by A2, FUNCT_1:def_3;
y = [(f1 . (pr1 s)),(f2 . (pr2 s))] by A7, A8;
hence y in [:A,B:] by A3, A10, A11, ZFMISC_1:87; ::_thesis: verum
end;
A12: for x, y, z being set st x in (arity f1) -tuples_on [:A,B:] & S1[x,y] & S1[x,z] holds
y = z
proof
let x, y, z be set ; ::_thesis: ( x in (arity f1) -tuples_on [:A,B:] & S1[x,y] & S1[x,z] implies y = z )
assume that
A13: x in (arity f1) -tuples_on [:A,B:] and
A14: S1[x,y] and
A15: S1[x,z] ; ::_thesis: y = z
consider s being Element of [:A,B:] * such that
A16: x = s and
len s = arity f1 by A13;
y = [(f1 . (pr1 s)),(f2 . (pr2 s))] by A14, A16;
hence y = z by A15, A16; ::_thesis: verum
end;
consider f being PartFunc of ((arity f1) -tuples_on [:A,B:]),[:A,B:] such that
A17: for x being set holds
( x in dom f iff ( x in (arity f1) -tuples_on [:A,B:] & ex y being set st S1[x,y] ) ) and
A18: for x being set st x in dom f holds
S1[x,f . x] from PARTFUN1:sch_2(A5, A12);
A19: dom f = (arity f1) -tuples_on [:A,B:]
proof
thus dom f c= (arity f1) -tuples_on [:A,B:] :: according to XBOOLE_0:def_10 ::_thesis: (arity f1) -tuples_on [:A,B:] c= dom f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom f or x in (arity f1) -tuples_on [:A,B:] )
assume x in dom f ; ::_thesis: x in (arity f1) -tuples_on [:A,B:]
hence x in (arity f1) -tuples_on [:A,B:] by A17; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (arity f1) -tuples_on [:A,B:] or x in dom f )
assume A20: x in (arity f1) -tuples_on [:A,B:] ; ::_thesis: x in dom f
then consider s being Element of [:A,B:] * such that
A21: x = s and
len s = arity f1 ;
now__::_thesis:_ex_y_being_set_st_
for_h_being_FinSequence_of_[:A,B:]_st_h_=_x_holds_
y_=_[(f1_._(pr1_h)),(f2_._(pr2_h))]
take y = [(f1 . (pr1 s)),(f2 . (pr2 s))]; ::_thesis: for h being FinSequence of [:A,B:] st h = x holds
y = [(f1 . (pr1 h)),(f2 . (pr2 h))]
let h be FinSequence of [:A,B:]; ::_thesis: ( h = x implies y = [(f1 . (pr1 h)),(f2 . (pr2 h))] )
assume h = x ; ::_thesis: y = [(f1 . (pr1 h)),(f2 . (pr2 h))]
hence y = [(f1 . (pr1 h)),(f2 . (pr2 h))] by A21; ::_thesis: verum
end;
hence x in dom f by A17, A20; ::_thesis: verum
end;
(arity f1) -tuples_on [:A,B:] in { (i -tuples_on [:A,B:]) where i is Element of NAT : verum } ;
then (arity f1) -tuples_on [:A,B:] c= union { (i -tuples_on [:A,B:]) where i is Element of NAT : verum } by ZFMISC_1:74;
then (arity f1) -tuples_on [:A,B:] c= [:A,B:] * by FINSEQ_2:108;
then reconsider f = f as PartFunc of ([:A,B:] *),[:A,B:] by RELSET_1:7;
A22: f is quasi_total
proof
let x, y be FinSequence of [:A,B:]; :: according to MARGREL1:def_22 ::_thesis: ( not len x = len y or not x in proj1 f or y in proj1 f )
assume that
A23: len x = len y and
A24: x in dom f ; ::_thesis: y in proj1 f
reconsider y9 = y as Element of [:A,B:] * by FINSEQ_1:def_11;
ex s1 being Element of [:A,B:] * st
( s1 = x & len s1 = arity f1 ) by A19, A24;
then y9 in { s where s is Element of [:A,B:] * : len s = arity f1 } by A23;
hence y in proj1 f by A19; ::_thesis: verum
end;
f is homogeneous
proof
let x, y be FinSequence; :: according to MARGREL1:def_1,MARGREL1:def_21 ::_thesis: ( not x in proj1 f or not y in proj1 f or len x = len y )
assume ( x in dom f & y in dom f ) ; ::_thesis: len x = len y
then ( ex s1 being Element of [:A,B:] * st
( s1 = x & len s1 = arity f1 ) & ex s2 being Element of [:A,B:] * st
( s2 = y & len s2 = arity f1 ) ) by A19;
hence len x = len y ; ::_thesis: verum
end;
then reconsider f = f as non empty homogeneous quasi_total PartFunc of ([:A,B:] *),[:A,B:] by A19, A22;
take f ; ::_thesis: ( dom f = (arity f1) -tuples_on [:A,B:] & ( for h being FinSequence of [:A,B:] st h in dom f holds
f . h = [(f1 . (pr1 h)),(f2 . (pr2 h))] ) )
thus dom f = (arity f1) -tuples_on [:A,B:] by A19; ::_thesis: for h being FinSequence of [:A,B:] st h in dom f holds
f . h = [(f1 . (pr1 h)),(f2 . (pr2 h))]
let h be FinSequence of [:A,B:]; ::_thesis: ( h in dom f implies f . h = [(f1 . (pr1 h)),(f2 . (pr2 h))] )
assume h in dom f ; ::_thesis: f . h = [(f1 . (pr1 h)),(f2 . (pr2 h))]
hence f . h = [(f1 . (pr1 h)),(f2 . (pr2 h))] by A18; ::_thesis: verum
end;
uniqueness
for b1, b2 being non empty homogeneous quasi_total PartFunc of ([:A,B:] *),[:A,B:] st dom b1 = (arity f1) -tuples_on [:A,B:] & ( for h being FinSequence of [:A,B:] st h in dom b1 holds
b1 . h = [(f1 . (pr1 h)),(f2 . (pr2 h))] ) & dom b2 = (arity f1) -tuples_on [:A,B:] & ( for h being FinSequence of [:A,B:] st h in dom b2 holds
b2 . h = [(f1 . (pr1 h)),(f2 . (pr2 h))] ) holds
b1 = b2
proof
let x, y be non empty homogeneous quasi_total PartFunc of ([:A,B:] *),[:A,B:]; ::_thesis: ( dom x = (arity f1) -tuples_on [:A,B:] & ( for h being FinSequence of [:A,B:] st h in dom x holds
x . h = [(f1 . (pr1 h)),(f2 . (pr2 h))] ) & dom y = (arity f1) -tuples_on [:A,B:] & ( for h being FinSequence of [:A,B:] st h in dom y holds
y . h = [(f1 . (pr1 h)),(f2 . (pr2 h))] ) implies x = y )
assume that
A25: dom x = (arity f1) -tuples_on [:A,B:] and
A26: for h being FinSequence of [:A,B:] st h in dom x holds
x . h = [(f1 . (pr1 h)),(f2 . (pr2 h))] and
A27: dom y = (arity f1) -tuples_on [:A,B:] and
A28: for h being FinSequence of [:A,B:] st h in dom y holds
y . h = [(f1 . (pr1 h)),(f2 . (pr2 h))] ; ::_thesis: x = y
now__::_thesis:_for_c_being_Element_of_[:A,B:]_*_st_c_in_dom_x_holds_
x_._c_=_y_._c
let c be Element of [:A,B:] * ; ::_thesis: ( c in dom x implies x . c = y . c )
reconsider c9 = c as FinSequence of [:A,B:] ;
assume A29: c in dom x ; ::_thesis: x . c = y . c
then x . c9 = [(f1 . (pr1 c9)),(f2 . (pr2 c9))] by A26;
hence x . c = y . c by A25, A27, A28, A29; ::_thesis: verum
end;
hence x = y by A25, A27, PARTFUN1:5; ::_thesis: verum
end;
end;
:: deftheorem Def3 defines [[: PRALG_1:def_3_:_
for A, B being non empty set
for f1 being non empty homogeneous quasi_total PartFunc of (A *),A
for f2 being non empty homogeneous quasi_total PartFunc of (B *),B st arity f1 = arity f2 holds
for b5 being non empty homogeneous quasi_total PartFunc of ([:A,B:] *),[:A,B:] holds
( b5 = [[:f1,f2:]] iff ( dom b5 = (arity f1) -tuples_on [:A,B:] & ( for h being FinSequence of [:A,B:] st h in dom b5 holds
b5 . h = [(f1 . (pr1 h)),(f2 . (pr2 h))] ) ) );
definition
let U1, U2 be Universal_Algebra;
assume A1: U1,U2 are_similar ;
func Opers (U1,U2) -> PFuncFinSequence of [: the carrier of U1, the carrier of U2:] means :Def4: :: PRALG_1:def 4
( len it = len the charact of U1 & ( for n being Nat st n in dom it holds
for h1 being non empty homogeneous quasi_total PartFunc of ( the carrier of U1 *), the carrier of U1
for h2 being non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2 st h1 = the charact of U1 . n & h2 = the charact of U2 . n holds
it . n = [[:h1,h2:]] ) );
existence
ex b1 being PFuncFinSequence of [: the carrier of U1, the carrier of U2:] st
( len b1 = len the charact of U1 & ( for n being Nat st n in dom b1 holds
for h1 being non empty homogeneous quasi_total PartFunc of ( the carrier of U1 *), the carrier of U1
for h2 being non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2 st h1 = the charact of U1 . n & h2 = the charact of U2 . n holds
b1 . n = [[:h1,h2:]] ) )
proof
defpred S1[ Nat, set ] means for h1 being non empty homogeneous quasi_total PartFunc of ( the carrier of U1 *), the carrier of U1
for h2 being non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2 st h1 = the charact of U1 . $1 & h2 = the charact of U2 . $1 holds
$2 = [[:h1,h2:]];
set l = len the charact of U1;
set c = [: the carrier of U1, the carrier of U2:];
A2: dom the charact of U2 = Seg (len the charact of U2) by FINSEQ_1:def_3;
A3: Seg (len the charact of U1) = dom the charact of U1 by FINSEQ_1:def_3;
A4: for m being Nat st m in Seg (len the charact of U1) holds
ex x being Element of PFuncs (([: the carrier of U1, the carrier of U2:] *),[: the carrier of U1, the carrier of U2:]) st S1[m,x]
proof
let m be Nat; ::_thesis: ( m in Seg (len the charact of U1) implies ex x being Element of PFuncs (([: the carrier of U1, the carrier of U2:] *),[: the carrier of U1, the carrier of U2:]) st S1[m,x] )
assume A5: m in Seg (len the charact of U1) ; ::_thesis: ex x being Element of PFuncs (([: the carrier of U1, the carrier of U2:] *),[: the carrier of U1, the carrier of U2:]) st S1[m,x]
then reconsider f1 = the charact of U1 . m as non empty homogeneous quasi_total PartFunc of ( the carrier of U1 *), the carrier of U1 by A3, MARGREL1:def_24, UNIALG_1:1;
len the charact of U1 = len the charact of U2 by A1, UNIALG_2:1;
then reconsider f2 = the charact of U2 . m as non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2 by A2, A5, MARGREL1:def_24, UNIALG_1:1;
reconsider F = [[:f1,f2:]] as Element of PFuncs (([: the carrier of U1, the carrier of U2:] *),[: the carrier of U1, the carrier of U2:]) by PARTFUN1:45;
take F ; ::_thesis: S1[m,F]
let h1 be non empty homogeneous quasi_total PartFunc of ( the carrier of U1 *), the carrier of U1; ::_thesis: for h2 being non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2 st h1 = the charact of U1 . m & h2 = the charact of U2 . m holds
F = [[:h1,h2:]]
let h2 be non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2; ::_thesis: ( h1 = the charact of U1 . m & h2 = the charact of U2 . m implies F = [[:h1,h2:]] )
assume ( h1 = the charact of U1 . m & h2 = the charact of U2 . m ) ; ::_thesis: F = [[:h1,h2:]]
hence F = [[:h1,h2:]] ; ::_thesis: verum
end;
consider p being FinSequence of PFuncs (([: the carrier of U1, the carrier of U2:] *),[: the carrier of U1, the carrier of U2:]) such that
A6: dom p = Seg (len the charact of U1) and
A7: for m being Nat st m in Seg (len the charact of U1) holds
S1[m,p . m] from FINSEQ_1:sch_5(A4);
reconsider p = p as PFuncFinSequence of [: the carrier of U1, the carrier of U2:] ;
take p ; ::_thesis: ( len p = len the charact of U1 & ( for n being Nat st n in dom p holds
for h1 being non empty homogeneous quasi_total PartFunc of ( the carrier of U1 *), the carrier of U1
for h2 being non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2 st h1 = the charact of U1 . n & h2 = the charact of U2 . n holds
p . n = [[:h1,h2:]] ) )
thus len p = len the charact of U1 by A6, FINSEQ_1:def_3; ::_thesis: for n being Nat st n in dom p holds
for h1 being non empty homogeneous quasi_total PartFunc of ( the carrier of U1 *), the carrier of U1
for h2 being non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2 st h1 = the charact of U1 . n & h2 = the charact of U2 . n holds
p . n = [[:h1,h2:]]
let n be Nat; ::_thesis: ( n in dom p implies for h1 being non empty homogeneous quasi_total PartFunc of ( the carrier of U1 *), the carrier of U1
for h2 being non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2 st h1 = the charact of U1 . n & h2 = the charact of U2 . n holds
p . n = [[:h1,h2:]] )
assume n in dom p ; ::_thesis: for h1 being non empty homogeneous quasi_total PartFunc of ( the carrier of U1 *), the carrier of U1
for h2 being non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2 st h1 = the charact of U1 . n & h2 = the charact of U2 . n holds
p . n = [[:h1,h2:]]
hence for h1 being non empty homogeneous quasi_total PartFunc of ( the carrier of U1 *), the carrier of U1
for h2 being non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2 st h1 = the charact of U1 . n & h2 = the charact of U2 . n holds
p . n = [[:h1,h2:]] by A6, A7; ::_thesis: verum
end;
uniqueness
for b1, b2 being PFuncFinSequence of [: the carrier of U1, the carrier of U2:] st len b1 = len the charact of U1 & ( for n being Nat st n in dom b1 holds
for h1 being non empty homogeneous quasi_total PartFunc of ( the carrier of U1 *), the carrier of U1
for h2 being non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2 st h1 = the charact of U1 . n & h2 = the charact of U2 . n holds
b1 . n = [[:h1,h2:]] ) & len b2 = len the charact of U1 & ( for n being Nat st n in dom b2 holds
for h1 being non empty homogeneous quasi_total PartFunc of ( the carrier of U1 *), the carrier of U1
for h2 being non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2 st h1 = the charact of U1 . n & h2 = the charact of U2 . n holds
b2 . n = [[:h1,h2:]] ) holds
b1 = b2
proof
let x, y be PFuncFinSequence of [: the carrier of U1, the carrier of U2:]; ::_thesis: ( len x = len the charact of U1 & ( for n being Nat st n in dom x holds
for h1 being non empty homogeneous quasi_total PartFunc of ( the carrier of U1 *), the carrier of U1
for h2 being non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2 st h1 = the charact of U1 . n & h2 = the charact of U2 . n holds
x . n = [[:h1,h2:]] ) & len y = len the charact of U1 & ( for n being Nat st n in dom y holds
for h1 being non empty homogeneous quasi_total PartFunc of ( the carrier of U1 *), the carrier of U1
for h2 being non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2 st h1 = the charact of U1 . n & h2 = the charact of U2 . n holds
y . n = [[:h1,h2:]] ) implies x = y )
assume that
A8: len x = len the charact of U1 and
A9: for n being Nat st n in dom x holds
for h1 being non empty homogeneous quasi_total PartFunc of ( the carrier of U1 *), the carrier of U1
for h2 being non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2 st h1 = the charact of U1 . n & h2 = the charact of U2 . n holds
x . n = [[:h1,h2:]] and
A10: len y = len the charact of U1 and
A11: for n being Nat st n in dom y holds
for h1 being non empty homogeneous quasi_total PartFunc of ( the carrier of U1 *), the carrier of U1
for h2 being non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2 st h1 = the charact of U1 . n & h2 = the charact of U2 . n holds
y . n = [[:h1,h2:]] ; ::_thesis: x = y
A12: dom x = Seg (len the charact of U1) by A8, FINSEQ_1:def_3;
now__::_thesis:_for_m_being_Nat_st_m_in_dom_x_holds_
x_._m_=_y_._m
let m be Nat; ::_thesis: ( m in dom x implies x . m = y . m )
assume A13: m in dom x ; ::_thesis: x . m = y . m
then m in dom the charact of U1 by A12, FINSEQ_1:def_3;
then reconsider h1 = the charact of U1 . m as non empty homogeneous quasi_total PartFunc of ( the carrier of U1 *), the carrier of U1 by MARGREL1:def_24, UNIALG_1:1;
Seg (len the charact of U2) = Seg (len the charact of U1) by A1, UNIALG_2:1;
then m in dom the charact of U2 by A12, A13, FINSEQ_1:def_3;
then reconsider h2 = the charact of U2 . m as non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2 by MARGREL1:def_24, UNIALG_1:1;
( m in dom y & x . m = [[:h1,h2:]] ) by A9, A10, A12, A13, FINSEQ_1:def_3;
hence x . m = y . m by A11; ::_thesis: verum
end;
hence x = y by A8, A10, FINSEQ_2:9; ::_thesis: verum
end;
end;
:: deftheorem Def4 defines Opers PRALG_1:def_4_:_
for U1, U2 being Universal_Algebra st U1,U2 are_similar holds
for b3 being PFuncFinSequence of [: the carrier of U1, the carrier of U2:] holds
( b3 = Opers (U1,U2) iff ( len b3 = len the charact of U1 & ( for n being Nat st n in dom b3 holds
for h1 being non empty homogeneous quasi_total PartFunc of ( the carrier of U1 *), the carrier of U1
for h2 being non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2 st h1 = the charact of U1 . n & h2 = the charact of U2 . n holds
b3 . n = [[:h1,h2:]] ) ) );
theorem Th1: :: PRALG_1:1
for U1, U2 being Universal_Algebra st U1,U2 are_similar holds
UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) is strict Universal_Algebra
proof
let U1, U2 be Universal_Algebra; ::_thesis: ( U1,U2 are_similar implies UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) is strict Universal_Algebra )
set C = UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #);
A1: dom (Opers (U1,U2)) = Seg (len (Opers (U1,U2))) by FINSEQ_1:def_3;
assume A2: U1,U2 are_similar ; ::_thesis: UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) is strict Universal_Algebra
then A3: ( dom the charact of U2 = Seg (len the charact of U2) & len the charact of U2 = len the charact of U1 ) by FINSEQ_1:def_3, UNIALG_2:1;
A4: len (Opers (U1,U2)) = len the charact of U1 by A2, Def4;
A5: dom the charact of U1 = Seg (len the charact of U1) by FINSEQ_1:def_3;
A6: the charact of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) is quasi_total
proof
let n be Nat; :: according to MARGREL1:def_24 ::_thesis: for b1 being Element of bool [:( the carrier of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) *), the carrier of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #):] holds
( not n in dom the charact of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) or not b1 = the charact of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) . n or b1 is quasi_total )
let h be PartFunc of ( the carrier of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) *), the carrier of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #); ::_thesis: ( not n in dom the charact of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) or not h = the charact of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) . n or h is quasi_total )
assume that
A7: n in dom the charact of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) and
A8: h = the charact of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) . n ; ::_thesis: h is quasi_total
reconsider h2 = the charact of U2 . n as non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2 by A1, A4, A3, A7, MARGREL1:def_24, UNIALG_1:1;
reconsider h1 = the charact of U1 . n as non empty homogeneous quasi_total PartFunc of ( the carrier of U1 *), the carrier of U1 by A1, A5, A4, A7, MARGREL1:def_24, UNIALG_1:1;
h = [[:h1,h2:]] by A2, A7, A8, Def4;
hence h is quasi_total ; ::_thesis: verum
end;
A9: the charact of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) is non-empty
proof
let n be set ; :: according to FUNCT_1:def_9 ::_thesis: ( not n in proj1 the charact of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) or not the charact of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) . n is empty )
set h = the charact of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) . n;
assume A10: n in dom the charact of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) ; ::_thesis: not the charact of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) . n is empty
then reconsider m = n as Element of NAT ;
reconsider h2 = the charact of U2 . m as non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2 by A1, A4, A3, A10, MARGREL1:def_24, UNIALG_1:1;
reconsider h1 = the charact of U1 . m as non empty homogeneous quasi_total PartFunc of ( the carrier of U1 *), the carrier of U1 by A1, A5, A4, A10, MARGREL1:def_24, UNIALG_1:1;
the charact of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) . n = [[:h1,h2:]] by A2, A10, Def4;
hence not the charact of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) . n is empty ; ::_thesis: verum
end;
A11: the charact of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) is homogeneous
proof
let n be Nat; :: according to MARGREL1:def_23 ::_thesis: for b1 being Element of bool [:( the carrier of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) *), the carrier of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #):] holds
( not n in dom the charact of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) or not b1 = the charact of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) . n or b1 is homogeneous )
let h be PartFunc of ( the carrier of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) *), the carrier of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #); ::_thesis: ( not n in dom the charact of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) or not h = the charact of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) . n or h is homogeneous )
assume that
A12: n in dom the charact of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) and
A13: h = the charact of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) . n ; ::_thesis: h is homogeneous
reconsider h2 = the charact of U2 . n as non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2 by A1, A4, A3, A12, MARGREL1:def_24, UNIALG_1:1;
reconsider h1 = the charact of U1 . n as non empty homogeneous quasi_total PartFunc of ( the carrier of U1 *), the carrier of U1 by A1, A5, A4, A12, MARGREL1:def_24, UNIALG_1:1;
h = [[:h1,h2:]] by A2, A12, A13, Def4;
hence h is homogeneous ; ::_thesis: verum
end;
the charact of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) <> {} by A4;
hence UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) is strict Universal_Algebra by A6, A11, A9, UNIALG_1:def_1, UNIALG_1:def_2, UNIALG_1:def_3; ::_thesis: verum
end;
definition
let U1, U2 be Universal_Algebra;
assume A1: U1,U2 are_similar ;
func[:U1,U2:] -> strict Universal_Algebra equals :Def5: :: PRALG_1:def 5
UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #);
coherence
UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) is strict Universal_Algebra by A1, Th1;
end;
:: deftheorem Def5 defines [: PRALG_1:def_5_:_
for U1, U2 being Universal_Algebra st U1,U2 are_similar holds
[:U1,U2:] = UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #);
definition
let A, B be non empty set ;
func Inv (A,B) -> Function of [:A,B:],[:B,A:] means :Def6: :: PRALG_1:def 6
for a being Element of [:A,B:] holds it . a = [(a `2),(a `1)];
existence
ex b1 being Function of [:A,B:],[:B,A:] st
for a being Element of [:A,B:] holds b1 . a = [(a `2),(a `1)]
proof
deffunc H1( Element of [:A,B:]) -> Element of [:B,A:] = [($1 `2),($1 `1)];
thus ex I being Function of [:A,B:],[:B,A:] st
for a being Element of [:A,B:] holds I . a = H1(a) from FUNCT_2:sch_4(); ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of [:A,B:],[:B,A:] st ( for a being Element of [:A,B:] holds b1 . a = [(a `2),(a `1)] ) & ( for a being Element of [:A,B:] holds b2 . a = [(a `2),(a `1)] ) holds
b1 = b2
proof
let f, g be Function of [:A,B:],[:B,A:]; ::_thesis: ( ( for a being Element of [:A,B:] holds f . a = [(a `2),(a `1)] ) & ( for a being Element of [:A,B:] holds g . a = [(a `2),(a `1)] ) implies f = g )
assume that
A1: for a being Element of [:A,B:] holds f . a = [(a `2),(a `1)] and
A2: for a being Element of [:A,B:] holds g . a = [(a `2),(a `1)] ; ::_thesis: f = g
now__::_thesis:_for_a_being_Element_of_[:A,B:]_holds_f_._a_=_g_._a
let a be Element of [:A,B:]; ::_thesis: f . a = g . a
f . a = [(a `2),(a `1)] by A1;
hence f . a = g . a by A2; ::_thesis: verum
end;
hence f = g by FUNCT_2:63; ::_thesis: verum
end;
end;
:: deftheorem Def6 defines Inv PRALG_1:def_6_:_
for A, B being non empty set
for b3 being Function of [:A,B:],[:B,A:] holds
( b3 = Inv (A,B) iff for a being Element of [:A,B:] holds b3 . a = [(a `2),(a `1)] );
theorem :: PRALG_1:2
for A, B being non empty set holds rng (Inv (A,B)) = [:B,A:]
proof
let A, B be non empty set ; ::_thesis: rng (Inv (A,B)) = [:B,A:]
thus rng (Inv (A,B)) c= [:B,A:] ; :: according to XBOOLE_0:def_10 ::_thesis: [:B,A:] c= rng (Inv (A,B))
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in [:B,A:] or x in rng (Inv (A,B)) )
A1: dom (Inv (A,B)) = [:A,B:] by FUNCT_2:def_1;
assume x in [:B,A:] ; ::_thesis: x in rng (Inv (A,B))
then reconsider y = x as Element of [:B,A:] ;
(Inv (A,B)) . [(y `2),(y `1)] = [([(y `2),(y `1)] `2),([(y `2),(y `1)] `1)] by Def6
.= [(y `1),([(y `2),(y `1)] `1)]
.= [(y `1),(y `2)]
.= y by MCART_1:21 ;
hence x in rng (Inv (A,B)) by A1, FUNCT_1:def_3; ::_thesis: verum
end;
theorem :: PRALG_1:3
for A, B being non empty set holds Inv (A,B) is one-to-one
proof
let A, B be non empty set ; ::_thesis: Inv (A,B) is one-to-one
let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds
( not x in proj1 (Inv (A,B)) or not b1 in proj1 (Inv (A,B)) or not (Inv (A,B)) . x = (Inv (A,B)) . b1 or x = b1 )
let y be set ; ::_thesis: ( not x in proj1 (Inv (A,B)) or not y in proj1 (Inv (A,B)) or not (Inv (A,B)) . x = (Inv (A,B)) . y or x = y )
assume that
A1: ( x in dom (Inv (A,B)) & y in dom (Inv (A,B)) ) and
A2: (Inv (A,B)) . x = (Inv (A,B)) . y ; ::_thesis: x = y
reconsider x1 = x, y1 = y as Element of [:A,B:] by A1, FUNCT_2:def_1;
( (Inv (A,B)) . x1 = [(x1 `2),(x1 `1)] & (Inv (A,B)) . y1 = [(y1 `2),(y1 `1)] ) by Def6;
then ( x1 `1 = y1 `1 & x1 `2 = y1 `2 ) by A2, XTUPLE_0:1;
hence x = y by DOMAIN_1:2; ::_thesis: verum
end;
theorem :: PRALG_1:4
for U1, U2 being Universal_Algebra st U1,U2 are_similar holds
Inv ( the carrier of U1, the carrier of U2) is Function of the carrier of [:U1,U2:], the carrier of [:U2,U1:]
proof
let U1, U2 be Universal_Algebra; ::_thesis: ( U1,U2 are_similar implies Inv ( the carrier of U1, the carrier of U2) is Function of the carrier of [:U1,U2:], the carrier of [:U2,U1:] )
assume U1,U2 are_similar ; ::_thesis: Inv ( the carrier of U1, the carrier of U2) is Function of the carrier of [:U1,U2:], the carrier of [:U2,U1:]
then ( [:U1,U2:] = UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) & [:U2,U1:] = UAStr(# [: the carrier of U2, the carrier of U1:],(Opers (U2,U1)) #) ) by Def5;
hence Inv ( the carrier of U1, the carrier of U2) is Function of the carrier of [:U1,U2:], the carrier of [:U2,U1:] ; ::_thesis: verum
end;
theorem Th5: :: PRALG_1:5
for U1, U2 being Universal_Algebra st U1,U2 are_similar holds
for o1 being operation of U1
for o2 being operation of U2
for o being operation of [:U1,U2:]
for n being Nat st o1 = the charact of U1 . n & o2 = the charact of U2 . n & o = the charact of [:U1,U2:] . n & n in dom the charact of U1 holds
( arity o = arity o1 & arity o = arity o2 & o = [[:o1,o2:]] )
proof
let U1, U2 be Universal_Algebra; ::_thesis: ( U1,U2 are_similar implies for o1 being operation of U1
for o2 being operation of U2
for o being operation of [:U1,U2:]
for n being Nat st o1 = the charact of U1 . n & o2 = the charact of U2 . n & o = the charact of [:U1,U2:] . n & n in dom the charact of U1 holds
( arity o = arity o1 & arity o = arity o2 & o = [[:o1,o2:]] ) )
assume A1: U1,U2 are_similar ; ::_thesis: for o1 being operation of U1
for o2 being operation of U2
for o being operation of [:U1,U2:]
for n being Nat st o1 = the charact of U1 . n & o2 = the charact of U2 . n & o = the charact of [:U1,U2:] . n & n in dom the charact of U1 holds
( arity o = arity o1 & arity o = arity o2 & o = [[:o1,o2:]] )
A2: dom (Opers (U1,U2)) = Seg (len (Opers (U1,U2))) by FINSEQ_1:def_3;
A3: dom the charact of U1 = Seg (len the charact of U1) by FINSEQ_1:def_3;
let o1 be operation of U1; ::_thesis: for o2 being operation of U2
for o being operation of [:U1,U2:]
for n being Nat st o1 = the charact of U1 . n & o2 = the charact of U2 . n & o = the charact of [:U1,U2:] . n & n in dom the charact of U1 holds
( arity o = arity o1 & arity o = arity o2 & o = [[:o1,o2:]] )
let o2 be operation of U2; ::_thesis: for o being operation of [:U1,U2:]
for n being Nat st o1 = the charact of U1 . n & o2 = the charact of U2 . n & o = the charact of [:U1,U2:] . n & n in dom the charact of U1 holds
( arity o = arity o1 & arity o = arity o2 & o = [[:o1,o2:]] )
let o be operation of [:U1,U2:]; ::_thesis: for n being Nat st o1 = the charact of U1 . n & o2 = the charact of U2 . n & o = the charact of [:U1,U2:] . n & n in dom the charact of U1 holds
( arity o = arity o1 & arity o = arity o2 & o = [[:o1,o2:]] )
let n be Nat; ::_thesis: ( o1 = the charact of U1 . n & o2 = the charact of U2 . n & o = the charact of [:U1,U2:] . n & n in dom the charact of U1 implies ( arity o = arity o1 & arity o = arity o2 & o = [[:o1,o2:]] ) )
assume that
A4: o1 = the charact of U1 . n and
A5: o2 = the charact of U2 . n and
A6: o = the charact of [:U1,U2:] . n and
A7: n in dom the charact of U1 ; ::_thesis: ( arity o = arity o1 & arity o = arity o2 & o = [[:o1,o2:]] )
A8: ( dom (signature U1) = Seg (len (signature U1)) & len (signature U1) = len the charact of U1 ) by FINSEQ_1:def_3, UNIALG_1:def_4;
then A9: (signature U1) . n = arity o1 by A4, A7, A3, UNIALG_1:def_4;
A10: signature U1 = signature U2 by A1, UNIALG_2:def_1;
then A11: (signature U2) . n = arity o2 by A5, A7, A3, A8, UNIALG_1:def_4;
A12: ( [:U1,U2:] = UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) & len the charact of U1 = len (Opers (U1,U2)) ) by A1, Def4, Def5;
then o = [[:o1,o2:]] by A1, A4, A5, A6, A7, A3, A2, Def4;
then A13: dom o = (arity o1) -tuples_on [: the carrier of U1, the carrier of U2:] by A10, A9, A11, Def3;
( ex x being FinSequence st x in dom o & ( for x being FinSequence st x in dom o holds
len x = arity o1 ) )
proof
set a = the Element of (arity o1) -tuples_on [: the carrier of U1, the carrier of U2:];
the Element of (arity o1) -tuples_on [: the carrier of U1, the carrier of U2:] in dom o by A13;
hence ex x being FinSequence st x in dom o ; ::_thesis: for x being FinSequence st x in dom o holds
len x = arity o1
let x be FinSequence; ::_thesis: ( x in dom o implies len x = arity o1 )
assume x in dom o ; ::_thesis: len x = arity o1
then ex s being Element of [: the carrier of U1, the carrier of U2:] * st
( s = x & len s = arity o1 ) by A13;
hence len x = arity o1 ; ::_thesis: verum
end;
hence ( arity o = arity o1 & arity o = arity o2 & o = [[:o1,o2:]] ) by A1, A4, A5, A6, A7, A3, A2, A12, A10, A9, A11, Def4, MARGREL1:def_25; ::_thesis: verum
end;
theorem :: PRALG_1:6
for U1, U2 being Universal_Algebra st U1,U2 are_similar holds
[:U1,U2:],U1 are_similar
proof
let U1, U2 be Universal_Algebra; ::_thesis: ( U1,U2 are_similar implies [:U1,U2:],U1 are_similar )
A1: dom (signature U1) = Seg (len (signature U1)) by FINSEQ_1:def_3;
A2: dom (signature U1) = Seg (len (signature U1)) by FINSEQ_1:def_3;
A3: dom the charact of [:U1,U2:] = Seg (len the charact of [:U1,U2:]) by FINSEQ_1:def_3;
A4: dom the charact of U2 = Seg (len the charact of U2) by FINSEQ_1:def_3;
A5: dom the charact of U1 = Seg (len the charact of U1) by FINSEQ_1:def_3;
assume A6: U1,U2 are_similar ; ::_thesis: [:U1,U2:],U1 are_similar
then [:U1,U2:] = UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) by Def5;
then len the charact of [:U1,U2:] = len the charact of U1 by A6, Def4;
then A7: len (signature [:U1,U2:]) = len the charact of U1 by UNIALG_1:def_4
.= len (signature U1) by UNIALG_1:def_4 ;
A8: dom (signature [:U1,U2:]) = Seg (len (signature [:U1,U2:])) by FINSEQ_1:def_3;
now__::_thesis:_for_n_being_Nat_st_n_in_dom_(signature_U1)_holds_
(signature_U1)_._n_=_(signature_[:U1,U2:])_._n
let n be Nat; ::_thesis: ( n in dom (signature U1) implies (signature U1) . n = (signature [:U1,U2:]) . n )
assume A9: n in dom (signature U1) ; ::_thesis: (signature U1) . n = (signature [:U1,U2:]) . n
then n in dom the charact of [:U1,U2:] by A7, A1, A3, UNIALG_1:def_4;
then reconsider o12 = the charact of [:U1,U2:] . n as operation of [:U1,U2:] by FUNCT_1:def_3;
len (signature U1) = len (signature U2) by A6, UNIALG_2:def_1
.= len the charact of U2 by UNIALG_1:def_4 ;
then reconsider o2 = the charact of U2 . n as operation of U2 by A1, A4, A9, FUNCT_1:def_3;
A10: o2 = the charact of U2 . n ;
A11: n in Seg (len the charact of U1) by A2, A9, UNIALG_1:def_4;
then n in dom the charact of U1 by FINSEQ_1:def_3;
then reconsider o1 = the charact of U1 . n as operation of U1 by FUNCT_1:def_3;
( (signature U1) . n = arity o1 & (signature [:U1,U2:]) . n = arity o12 ) by A7, A1, A8, A9, UNIALG_1:def_4;
hence (signature U1) . n = (signature [:U1,U2:]) . n by A6, A5, A11, A10, Th5; ::_thesis: verum
end;
then signature U1 = signature [:U1,U2:] by A7, FINSEQ_2:9;
hence [:U1,U2:],U1 are_similar by UNIALG_2:def_1; ::_thesis: verum
end;
theorem :: PRALG_1:7
for U1, U2, U3, U4 being Universal_Algebra st U1 is SubAlgebra of U2 & U3 is SubAlgebra of U4 & U2,U4 are_similar holds
[:U1,U3:] is SubAlgebra of [:U2,U4:]
proof
let U1, U2, U3, U4 be Universal_Algebra; ::_thesis: ( U1 is SubAlgebra of U2 & U3 is SubAlgebra of U4 & U2,U4 are_similar implies [:U1,U3:] is SubAlgebra of [:U2,U4:] )
assume that
A1: U1 is SubAlgebra of U2 and
A2: U3 is SubAlgebra of U4 and
A3: U2,U4 are_similar ; ::_thesis: [:U1,U3:] is SubAlgebra of [:U2,U4:]
A4: [:U2,U4:] = UAStr(# [: the carrier of U2, the carrier of U4:],(Opers (U2,U4)) #) by A3, Def5;
A5: U1,U2 are_similar by A1, UNIALG_2:13;
then A6: U1,U4 are_similar by A3, UNIALG_2:2;
A7: U3,U4 are_similar by A2, UNIALG_2:13;
then A8: [:U1,U3:] = UAStr(# [: the carrier of U1, the carrier of U3:],(Opers (U1,U3)) #) by A6, Def5, UNIALG_2:2;
A9: ( the carrier of U1 is Subset of U2 & the carrier of U3 is Subset of U4 ) by A1, A2, UNIALG_2:def_7;
hence the carrier of [:U1,U3:] is Subset of [:U2,U4:] by A8, A4, ZFMISC_1:96; :: according to UNIALG_2:def_7 ::_thesis: for b1 being Element of bool the carrier of [:U2,U4:] holds
( not b1 = the carrier of [:U1,U3:] or ( the charact of [:U1,U3:] = Opers ([:U2,U4:],b1) & b1 is opers_closed ) )
let B be non empty Subset of [:U2,U4:]; ::_thesis: ( not B = the carrier of [:U1,U3:] or ( the charact of [:U1,U3:] = Opers ([:U2,U4:],B) & B is opers_closed ) )
assume A10: B = the carrier of [:U1,U3:] ; ::_thesis: ( the charact of [:U1,U3:] = Opers ([:U2,U4:],B) & B is opers_closed )
signature U4 = signature U2 by A3, UNIALG_2:def_1;
then len the charact of U4 = len (signature U2) by UNIALG_1:def_4;
then A11: ( dom the charact of U4 = Seg (len the charact of U4) & len the charact of U4 = len the charact of U2 ) by FINSEQ_1:def_3, UNIALG_1:def_4;
A12: dom the charact of U1 = Seg (len the charact of U1) by FINSEQ_1:def_3;
A13: dom the charact of U2 = Seg (len the charact of U2) by FINSEQ_1:def_3;
A14: U1,U3 are_similar by A7, A6, UNIALG_2:2;
then A15: len the charact of [:U1,U3:] = len the charact of U1 by A8, Def4;
signature U1 = signature U3 by A14, UNIALG_2:def_1;
then len the charact of U1 = len (signature U3) by UNIALG_1:def_4;
then A16: ( dom the charact of U3 = Seg (len the charact of U3) & len the charact of U1 = len the charact of U3 ) by FINSEQ_1:def_3, UNIALG_1:def_4;
A17: dom (Opers ([:U2,U4:],B)) = Seg (len (Opers ([:U2,U4:],B))) by FINSEQ_1:def_3;
A18: dom the charact of [:U2,U4:] = dom (Opers ([:U2,U4:],B)) by UNIALG_2:def_6;
then len the charact of [:U2,U4:] = len (Opers ([:U2,U4:],B)) by FINSEQ_3:29;
then A19: len the charact of U2 = len (Opers ([:U2,U4:],B)) by A3, A4, Def4;
signature U1 = signature U2 by A5, UNIALG_2:def_1;
then len the charact of U1 = len (signature U2) by UNIALG_1:def_4;
then A20: len the charact of [:U1,U3:] = len (Opers ([:U2,U4:],B)) by A19, A15, UNIALG_1:def_4;
reconsider B3 = the carrier of U3 as non empty Subset of U4 by A2, UNIALG_2:def_7;
A21: B3 is opers_closed by A2, UNIALG_2:def_7;
reconsider B1 = the carrier of U1 as non empty Subset of U2 by A1, UNIALG_2:def_7;
A22: B1 is opers_closed by A1, UNIALG_2:def_7;
A23: [: the carrier of U1, the carrier of U3:] c= [: the carrier of U2, the carrier of U4:] by A9, ZFMISC_1:96;
A24: for o being operation of [:U2,U4:] holds B is_closed_on o
proof
let o be operation of [:U2,U4:]; ::_thesis: B is_closed_on o
let s be FinSequence of B; :: according to UNIALG_2:def_3 ::_thesis: ( not len s = arity o or o . s in B )
reconsider s0 = s as Element of [: the carrier of U1, the carrier of U3:] * by A8, A10, FINSEQ_1:def_11;
consider n being Nat such that
A25: n in dom the charact of [:U2,U4:] and
A26: the charact of [:U2,U4:] . n = o by FINSEQ_2:10;
reconsider s3 = pr2 s0 as Element of B3 * by FINSEQ_1:def_11;
reconsider s1 = pr1 s0 as Element of B1 * by FINSEQ_1:def_11;
A27: len the charact of [:U2,U4:] = len the charact of U2 by A3, A4, Def4;
A28: n in Seg (len the charact of [:U2,U4:]) by A25, FINSEQ_1:def_3;
then A29: n in dom the charact of U2 by A27, FINSEQ_1:def_3;
then reconsider o2 = the charact of U2 . n as operation of U2 by FUNCT_1:def_3;
len the charact of U4 = len the charact of U2 by A3, UNIALG_2:1;
then n in dom the charact of U4 by A28, A27, FINSEQ_1:def_3;
then reconsider o4 = the charact of U4 . n as operation of U4 by FUNCT_1:def_3;
A30: o = [[:o2,o4:]] by A3, A26, A29, Th5;
o4 = the charact of U4 . n ;
then A31: arity o = arity o2 by A3, A26, A29, Th5;
rng s0 c= [: the carrier of U1, the carrier of U3:] by FINSEQ_1:def_4;
then rng s0 c= [: the carrier of U2, the carrier of U4:] by A23, XBOOLE_1:1;
then s0 is FinSequence of [: the carrier of U2, the carrier of U4:] by FINSEQ_1:def_4;
then reconsider ss = s0 as Element of [: the carrier of U2, the carrier of U4:] * by FINSEQ_1:def_11;
o2 = the charact of U2 . n ;
then A32: arity o = arity o4 by A3, A26, A29, Th5;
assume A33: len s = arity o ; ::_thesis: o . s in B
then A34: ss in { w where w is Element of [: the carrier of U2, the carrier of U4:] * : len w = arity o2 } by A31;
( B3 is_closed_on o4 & len s3 = len s0 ) by A21, Def2, UNIALG_2:def_4;
then A35: o4 . s3 in B3 by A33, A32, UNIALG_2:def_3;
( B1 is_closed_on o2 & len s1 = len s0 ) by A22, Def1, UNIALG_2:def_4;
then A36: o2 . s1 in B1 by A33, A31, UNIALG_2:def_3;
dom [[:o2,o4:]] = (arity o2) -tuples_on [: the carrier of U2, the carrier of U4:] by A31, A32, Def3;
then o . s = [(o2 . (pr1 ss)),(o4 . (pr2 ss))] by A31, A32, A30, A34, Def3;
hence o . s in B by A8, A10, A36, A35, ZFMISC_1:87; ::_thesis: verum
end;
A37: dom the charact of U4 = dom (Opers (U4,B3)) by UNIALG_2:def_6;
A38: dom the charact of [:U1,U3:] = Seg (len the charact of [:U1,U3:]) by FINSEQ_1:def_3;
A39: dom the charact of U2 = dom (Opers (U2,B1)) by UNIALG_2:def_6;
for n being Nat st n in dom the charact of [:U1,U3:] holds
the charact of [:U1,U3:] . n = (Opers ([:U2,U4:],B)) . n
proof
let n be Nat; ::_thesis: ( n in dom the charact of [:U1,U3:] implies the charact of [:U1,U3:] . n = (Opers ([:U2,U4:],B)) . n )
assume A40: n in dom the charact of [:U1,U3:] ; ::_thesis: the charact of [:U1,U3:] . n = (Opers ([:U2,U4:],B)) . n
then reconsider o2 = the charact of U2 . n as operation of U2 by A19, A20, A13, A38, FUNCT_1:def_3;
reconsider o4 = the charact of U4 . n as operation of U4 by A19, A20, A38, A11, A40, FUNCT_1:def_3;
reconsider o24 = the charact of [:U2,U4:] . n as operation of [:U2,U4:] by A18, A20, A38, A17, A40, FUNCT_1:def_3;
A41: o24 = [[:o2,o4:]] by A3, A19, A20, A13, A38, A40, Th5;
reconsider o3 = the charact of U3 . n as operation of U3 by A15, A38, A16, A40, FUNCT_1:def_3;
(Opers (U4,B3)) . n = o4 /. B3 by A19, A20, A38, A11, A37, A40, UNIALG_2:def_6;
then A42: o3 = o4 /. B3 by A2, UNIALG_2:def_7;
o2 = the charact of U2 . n ;
then A43: arity o24 = arity o4 by A3, A19, A20, A13, A38, A40, Th5;
reconsider o1 = the charact of U1 . n as operation of U1 by A15, A12, A38, A40, FUNCT_1:def_3;
(Opers (U2,B1)) . n = o2 /. B1 by A19, A20, A13, A38, A39, A40, UNIALG_2:def_6;
then A44: o1 = o2 /. B1 by A1, UNIALG_2:def_7;
A45: B3 is_closed_on o4 by A21, UNIALG_2:def_4;
then A46: arity (o4 /. B3) = arity o4 by UNIALG_2:5;
o4 = the charact of U4 . n ;
then A47: arity o24 = arity o2 by A3, A19, A20, A13, A38, A40, Th5;
then A48: dom ([[:o2,o4:]] | ((arity o24) -tuples_on B)) = (dom [[:o2,o4:]]) /\ ((arity o2) -tuples_on B) by RELAT_1:61
.= ((arity o2) -tuples_on the carrier of [:U2,U4:]) /\ ((arity o2) -tuples_on B) by A4, A43, A47, Def3
.= (arity o2) -tuples_on B by MARGREL1:21 ;
A49: B1 is_closed_on o2 by A22, UNIALG_2:def_4;
then A50: arity (o2 /. B1) = arity o2 by UNIALG_2:5;
then A51: dom [[:(o2 /. B1),(o4 /. B3):]] = (arity o2) -tuples_on B by A8, A10, A43, A47, A46, Def3;
A52: now__::_thesis:_for_x_being_set_st_x_in_(arity_o2)_-tuples_on_B_holds_
[[:(o2_/._B1),(o4_/._B3):]]_._x_=_([[:o2,o4:]]_|_((arity_o24)_-tuples_on_B))_._x
let x be set ; ::_thesis: ( x in (arity o2) -tuples_on B implies [[:(o2 /. B1),(o4 /. B3):]] . x = ([[:o2,o4:]] | ((arity o24) -tuples_on B)) . x )
A53: dom ([[:o2,o4:]] | ((arity o24) -tuples_on B)) c= dom [[:o2,o4:]] by RELAT_1:60;
assume A54: x in (arity o2) -tuples_on B ; ::_thesis: [[:(o2 /. B1),(o4 /. B3):]] . x = ([[:o2,o4:]] | ((arity o24) -tuples_on B)) . x
then consider s being Element of B * such that
A55: s = x and
A56: len s = arity o2 ;
rng s c= B by FINSEQ_1:def_4;
then rng s c= [: the carrier of U2, the carrier of U4:] by A4, XBOOLE_1:1;
then reconsider s0 = s as FinSequence of [: the carrier of U2, the carrier of U4:] by FINSEQ_1:def_4;
A57: ([[:o2,o4:]] | ((arity o24) -tuples_on B)) . x = [[:o2,o4:]] . s0 by A48, A54, A55, FUNCT_1:47
.= [(o2 . (pr1 s0)),(o4 . (pr2 s0))] by A43, A47, A48, A54, A55, A53, Def3 ;
reconsider s1 = s as FinSequence of [:B1,B3:] by A8, A10;
reconsider s11 = pr1 s1 as Element of B1 * by FINSEQ_1:def_11;
len (pr1 s1) = len s1 by Def1;
then A58: s11 in { a where a is Element of B1 * : len a = arity o2 } by A56;
reconsider s12 = pr2 s1 as Element of B3 * by FINSEQ_1:def_11;
len (pr2 s1) = len s1 by Def2;
then A59: s12 in { b where b is Element of B3 * : len b = arity o4 } by A43, A47, A56;
A60: dom (o4 | ((arity o4) -tuples_on B3)) = (dom o4) /\ ((arity o4) -tuples_on B3) by RELAT_1:61
.= ((arity o4) -tuples_on the carrier of U4) /\ ((arity o4) -tuples_on B3) by MARGREL1:22
.= (arity o4) -tuples_on B3 by MARGREL1:21 ;
A61: dom (o2 | ((arity o2) -tuples_on B1)) = (dom o2) /\ ((arity o2) -tuples_on B1) by RELAT_1:61
.= ((arity o2) -tuples_on the carrier of U2) /\ ((arity o2) -tuples_on B1) by MARGREL1:22
.= (arity o2) -tuples_on B1 by MARGREL1:21 ;
[[:(o2 /. B1),(o4 /. B3):]] . x = [((o2 /. B1) . (pr1 s1)),((o4 /. B3) . (pr2 s1))] by A43, A47, A50, A46, A51, A54, A55, Def3
.= [((o2 | ((arity o2) -tuples_on B1)) . s11),((o4 /. B3) . (pr2 s1))] by A49, UNIALG_2:def_5
.= [(o2 . (pr1 s1)),((o4 /. B3) . (pr2 s1))] by A58, A61, FUNCT_1:47
.= [(o2 . (pr1 s1)),((o4 | ((arity o4) -tuples_on B3)) . (pr2 s1))] by A45, UNIALG_2:def_5
.= [(o2 . (pr1 s1)),(o4 . (pr2 s1))] by A59, A60, FUNCT_1:47 ;
hence [[:(o2 /. B1),(o4 /. B3):]] . x = ([[:o2,o4:]] | ((arity o24) -tuples_on B)) . x by A57; ::_thesis: verum
end;
thus (Opers ([:U2,U4:],B)) . n = o24 /. B by A20, A38, A17, A40, UNIALG_2:def_6
.= [[:o2,o4:]] | ((arity o24) -tuples_on B) by A24, A41, UNIALG_2:def_5
.= [[:(o2 /. B1),(o4 /. B3):]] by A51, A48, A52, FUNCT_1:2
.= the charact of [:U1,U3:] . n by A14, A8, A40, A44, A42, Def4 ; ::_thesis: verum
end;
hence ( the charact of [:U1,U3:] = Opers ([:U2,U4:],B) & B is opers_closed ) by A24, A20, FINSEQ_2:9, UNIALG_2:def_4; ::_thesis: verum
end;
begin
definition
let k be Nat;
func TrivialOp k -> PartFunc of ({{}} *),{{}} means :Def7: :: PRALG_1:def 7
( dom it = {(k |-> {})} & rng it = {{}} );
existence
ex b1 being PartFunc of ({{}} *),{{}} st
( dom b1 = {(k |-> {})} & rng b1 = {{}} )
proof
consider f being Function such that
A1: dom f = {(k |-> {})} and
A2: rng f = {{}} by FUNCT_1:5;
dom f c= {{}} *
proof
reconsider a = {} as Element of {{}} by TARSKI:def_1;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom f or x in {{}} * )
assume x in dom f ; ::_thesis: x in {{}} *
then x = k |-> a by A1, TARSKI:def_1;
hence x in {{}} * by FINSEQ_1:def_11; ::_thesis: verum
end;
then reconsider f = f as PartFunc of ({{}} *),{{}} by A2, RELSET_1:4;
take f ; ::_thesis: ( dom f = {(k |-> {})} & rng f = {{}} )
thus ( dom f = {(k |-> {})} & rng f = {{}} ) by A1, A2; ::_thesis: verum
end;
uniqueness
for b1, b2 being PartFunc of ({{}} *),{{}} st dom b1 = {(k |-> {})} & rng b1 = {{}} & dom b2 = {(k |-> {})} & rng b2 = {{}} holds
b1 = b2 by FUNCT_1:7;
end;
:: deftheorem Def7 defines TrivialOp PRALG_1:def_7_:_
for k being Nat
for b2 being PartFunc of ({{}} *),{{}} holds
( b2 = TrivialOp k iff ( dom b2 = {(k |-> {})} & rng b2 = {{}} ) );
registration
let k be Nat;
cluster TrivialOp k -> non empty homogeneous quasi_total ;
coherence
( TrivialOp k is homogeneous & TrivialOp k is quasi_total & not TrivialOp k is empty )
proof
set f = TrivialOp k;
A1: dom (TrivialOp k) = {(k |-> {})} by Def7;
thus TrivialOp k is homogeneous ::_thesis: ( TrivialOp k is quasi_total & not TrivialOp k is empty )
proof
let x, y be FinSequence; :: according to MARGREL1:def_1,MARGREL1:def_21 ::_thesis: ( not x in proj1 (TrivialOp k) or not y in proj1 (TrivialOp k) or len x = len y )
assume that
A2: x in dom (TrivialOp k) and
A3: y in dom (TrivialOp k) ; ::_thesis: len x = len y
x = k |-> {} by A1, A2, TARSKI:def_1;
hence len x = len y by A1, A3, TARSKI:def_1; ::_thesis: verum
end;
now__::_thesis:_for_x,_y_being_FinSequence_of_{{}}_st_len_x_=_len_y_&_x_in_dom_(TrivialOp_k)_holds_
y_in_dom_(TrivialOp_k)
let x, y be FinSequence of {{}}; ::_thesis: ( len x = len y & x in dom (TrivialOp k) implies y in dom (TrivialOp k) )
assume that
A4: len x = len y and
A5: x in dom (TrivialOp k) ; ::_thesis: y in dom (TrivialOp k)
A6: dom x = Seg (len x) by FINSEQ_1:def_3;
A7: x = k |-> {} by A1, A5, TARSKI:def_1;
now__::_thesis:_for_n_being_Nat_st_n_in_dom_x_holds_
x_._n_=_y_._n
let n be Nat; ::_thesis: ( n in dom x implies x . n = y . n )
assume n in dom x ; ::_thesis: x . n = y . n
then n in dom y by A4, A6, FINSEQ_1:def_3;
then A8: y . n in {{}} by FINSEQ_2:11;
x . n = {} by A7;
hence x . n = y . n by A8, TARSKI:def_1; ::_thesis: verum
end;
hence y in dom (TrivialOp k) by A4, A5, FINSEQ_2:9; ::_thesis: verum
end;
hence ( TrivialOp k is quasi_total & not TrivialOp k is empty ) by A1, MARGREL1:def_22; ::_thesis: verum
end;
end;
theorem :: PRALG_1:8
for k being Nat holds arity (TrivialOp k) = k
proof
let k be Nat; ::_thesis: arity (TrivialOp k) = k
now__::_thesis:_(_ex_x_being_FinSequence_st_x_in_dom_(TrivialOp_k)_&_(_for_x_being_FinSequence_st_x_in_dom_(TrivialOp_k)_holds_
len_x_=_k_)_)
dom (TrivialOp k) = {(k |-> {})} by Def7;
then k |-> {} in dom (TrivialOp k) by TARSKI:def_1;
hence ex x being FinSequence st x in dom (TrivialOp k) ; ::_thesis: for x being FinSequence st x in dom (TrivialOp k) holds
len x = k
let x be FinSequence; ::_thesis: ( x in dom (TrivialOp k) implies len x = k )
assume x in dom (TrivialOp k) ; ::_thesis: len x = k
then x in {(k |-> {})} by Def7;
then x = k |-> {} by TARSKI:def_1;
hence len x = k by CARD_1:def_7; ::_thesis: verum
end;
hence arity (TrivialOp k) = k by MARGREL1:def_25; ::_thesis: verum
end;
definition
let f be FinSequence of NAT ;
func TrivialOps f -> PFuncFinSequence of {{}} means :Def8: :: PRALG_1:def 8
( len it = len f & ( for n being Nat st n in dom it holds
for m being Nat st m = f . n holds
it . n = TrivialOp m ) );
existence
ex b1 being PFuncFinSequence of {{}} st
( len b1 = len f & ( for n being Nat st n in dom b1 holds
for m being Nat st m = f . n holds
b1 . n = TrivialOp m ) )
proof
defpred S1[ set , set ] means for m being Nat st m = f . $1 holds
$2 = TrivialOp m;
A1: for k being Nat st k in Seg (len f) holds
ex x being Element of PFuncs (({{}} *),{{}}) st S1[k,x]
proof
let k be Nat; ::_thesis: ( k in Seg (len f) implies ex x being Element of PFuncs (({{}} *),{{}}) st S1[k,x] )
assume k in Seg (len f) ; ::_thesis: ex x being Element of PFuncs (({{}} *),{{}}) st S1[k,x]
then k in dom f by FINSEQ_1:def_3;
then reconsider k1 = f . k as Element of NAT by FINSEQ_2:11;
reconsider A = TrivialOp k1 as Element of PFuncs (({{}} *),{{}}) by PARTFUN1:45;
take A ; ::_thesis: S1[k,A]
let m be Nat; ::_thesis: ( m = f . k implies A = TrivialOp m )
assume m = f . k ; ::_thesis: A = TrivialOp m
hence A = TrivialOp m ; ::_thesis: verum
end;
consider p being FinSequence of PFuncs (({{}} *),{{}}) such that
A2: ( dom p = Seg (len f) & ( for k being Nat st k in Seg (len f) holds
S1[k,p . k] ) ) from FINSEQ_1:sch_5(A1);
reconsider p = p as PFuncFinSequence of {{}} ;
take p ; ::_thesis: ( len p = len f & ( for n being Nat st n in dom p holds
for m being Nat st m = f . n holds
p . n = TrivialOp m ) )
thus len p = len f by A2, FINSEQ_1:def_3; ::_thesis: for n being Nat st n in dom p holds
for m being Nat st m = f . n holds
p . n = TrivialOp m
let n be Nat; ::_thesis: ( n in dom p implies for m being Nat st m = f . n holds
p . n = TrivialOp m )
assume n in dom p ; ::_thesis: for m being Nat st m = f . n holds
p . n = TrivialOp m
hence for m being Nat st m = f . n holds
p . n = TrivialOp m by A2; ::_thesis: verum
end;
uniqueness
for b1, b2 being PFuncFinSequence of {{}} st len b1 = len f & ( for n being Nat st n in dom b1 holds
for m being Nat st m = f . n holds
b1 . n = TrivialOp m ) & len b2 = len f & ( for n being Nat st n in dom b2 holds
for m being Nat st m = f . n holds
b2 . n = TrivialOp m ) holds
b1 = b2
proof
let x, y be PFuncFinSequence of {{}}; ::_thesis: ( len x = len f & ( for n being Nat st n in dom x holds
for m being Nat st m = f . n holds
x . n = TrivialOp m ) & len y = len f & ( for n being Nat st n in dom y holds
for m being Nat st m = f . n holds
y . n = TrivialOp m ) implies x = y )
assume that
A3: len x = len f and
A4: for n being Nat st n in dom x holds
for m being Nat st m = f . n holds
x . n = TrivialOp m and
A5: len y = len f and
A6: for n being Nat st n in dom y holds
for m being Nat st m = f . n holds
y . n = TrivialOp m ; ::_thesis: x = y
A7: dom x = Seg (len f) by A3, FINSEQ_1:def_3;
now__::_thesis:_for_n_being_Nat_st_n_in_dom_x_holds_
x_._n_=_y_._n
let n be Nat; ::_thesis: ( n in dom x implies x . n = y . n )
assume A8: n in dom x ; ::_thesis: x . n = y . n
then n in dom f by A7, FINSEQ_1:def_3;
then reconsider m = f . n as Element of NAT by FINSEQ_2:11;
( n in dom y & x . n = TrivialOp m ) by A4, A5, A7, A8, FINSEQ_1:def_3;
hence x . n = y . n by A6; ::_thesis: verum
end;
hence x = y by A3, A5, FINSEQ_2:9; ::_thesis: verum
end;
end;
:: deftheorem Def8 defines TrivialOps PRALG_1:def_8_:_
for f being FinSequence of NAT
for b2 being PFuncFinSequence of {{}} holds
( b2 = TrivialOps f iff ( len b2 = len f & ( for n being Nat st n in dom b2 holds
for m being Nat st m = f . n holds
b2 . n = TrivialOp m ) ) );
theorem Th9: :: PRALG_1:9
for f being FinSequence of NAT holds
( TrivialOps f is homogeneous & TrivialOps f is quasi_total & TrivialOps f is non-empty )
proof
let f be FinSequence of NAT ; ::_thesis: ( TrivialOps f is homogeneous & TrivialOps f is quasi_total & TrivialOps f is non-empty )
A1: for n being Nat
for h being PartFunc of ({{}} *),{{}} st n in dom (TrivialOps f) & h = (TrivialOps f) . n holds
h is quasi_total
proof
let n be Nat; ::_thesis: for h being PartFunc of ({{}} *),{{}} st n in dom (TrivialOps f) & h = (TrivialOps f) . n holds
h is quasi_total
let h be PartFunc of ({{}} *),{{}}; ::_thesis: ( n in dom (TrivialOps f) & h = (TrivialOps f) . n implies h is quasi_total )
assume that
A2: n in dom (TrivialOps f) and
A3: (TrivialOps f) . n = h ; ::_thesis: h is quasi_total
dom (TrivialOps f) = Seg (len (TrivialOps f)) by FINSEQ_1:def_3
.= Seg (len f) by Def8
.= dom f by FINSEQ_1:def_3 ;
then reconsider m = f . n as Element of NAT by A2, FINSEQ_2:11;
(TrivialOps f) . n = TrivialOp m by A2, Def8;
hence h is quasi_total by A3; ::_thesis: verum
end;
A4: for n being set st n in dom (TrivialOps f) holds
not (TrivialOps f) . n is empty
proof
let n be set ; ::_thesis: ( n in dom (TrivialOps f) implies not (TrivialOps f) . n is empty )
assume A5: n in dom (TrivialOps f) ; ::_thesis: not (TrivialOps f) . n is empty
then reconsider k = n as Element of NAT ;
dom (TrivialOps f) = Seg (len (TrivialOps f)) by FINSEQ_1:def_3
.= Seg (len f) by Def8
.= dom f by FINSEQ_1:def_3 ;
then reconsider m = f . k as Element of NAT by A5, FINSEQ_2:11;
(TrivialOps f) . k = TrivialOp m by A5, Def8;
hence not (TrivialOps f) . n is empty ; ::_thesis: verum
end;
for n being Nat
for h being PartFunc of ({{}} *),{{}} st n in dom (TrivialOps f) & h = (TrivialOps f) . n holds
h is homogeneous
proof
let n be Nat; ::_thesis: for h being PartFunc of ({{}} *),{{}} st n in dom (TrivialOps f) & h = (TrivialOps f) . n holds
h is homogeneous
let h be PartFunc of ({{}} *),{{}}; ::_thesis: ( n in dom (TrivialOps f) & h = (TrivialOps f) . n implies h is homogeneous )
assume that
A6: n in dom (TrivialOps f) and
A7: (TrivialOps f) . n = h ; ::_thesis: h is homogeneous
dom (TrivialOps f) = Seg (len (TrivialOps f)) by FINSEQ_1:def_3
.= Seg (len f) by Def8
.= dom f by FINSEQ_1:def_3 ;
then reconsider m = f . n as Element of NAT by A6, FINSEQ_2:11;
(TrivialOps f) . n = TrivialOp m by A6, Def8;
hence h is homogeneous by A7; ::_thesis: verum
end;
hence ( TrivialOps f is homogeneous & TrivialOps f is quasi_total & TrivialOps f is non-empty ) by A1, A4, FUNCT_1:def_9, MARGREL1:def_23, MARGREL1:def_24; ::_thesis: verum
end;
theorem Th10: :: PRALG_1:10
for f being FinSequence of NAT st f <> {} holds
UAStr(# {{}},(TrivialOps f) #) is strict Universal_Algebra
proof
let f be FinSequence of NAT ; ::_thesis: ( f <> {} implies UAStr(# {{}},(TrivialOps f) #) is strict Universal_Algebra )
assume A1: f <> {} ; ::_thesis: UAStr(# {{}},(TrivialOps f) #) is strict Universal_Algebra
set U0 = UAStr(# {{}},(TrivialOps f) #);
A2: ( the charact of UAStr(# {{}},(TrivialOps f) #) is homogeneous & the charact of UAStr(# {{}},(TrivialOps f) #) is quasi_total & the charact of UAStr(# {{}},(TrivialOps f) #) is non-empty ) by Th9;
len the charact of UAStr(# {{}},(TrivialOps f) #) = len f by Def8;
then the charact of UAStr(# {{}},(TrivialOps f) #) <> {} by A1;
hence UAStr(# {{}},(TrivialOps f) #) is strict Universal_Algebra by A2, UNIALG_1:def_1, UNIALG_1:def_2, UNIALG_1:def_3; ::_thesis: verum
end;
registration
let D be non empty set ;
cluster Relation-like NAT -defined D -valued Function-like non empty V31() countable FinSequence-like FinSubsequence-like for Element of D * ;
existence
not for b1 being Element of D * holds b1 is empty
proof
set d = the Element of D;
reconsider e = <* the Element of D*> as Element of D * by FINSEQ_1:def_11;
take e ; ::_thesis: not e is empty
thus not e is empty ; ::_thesis: verum
end;
end;
definition
let f be non empty FinSequence of NAT ;
func Trivial_Algebra f -> strict Universal_Algebra equals :: PRALG_1:def 9
UAStr(# {{}},(TrivialOps f) #);
coherence
UAStr(# {{}},(TrivialOps f) #) is strict Universal_Algebra by Th10;
end;
:: deftheorem defines Trivial_Algebra PRALG_1:def_9_:_
for f being non empty FinSequence of NAT holds Trivial_Algebra f = UAStr(# {{}},(TrivialOps f) #);
begin
definition
let IT be Function;
attrIT is Univ_Alg-yielding means :Def10: :: PRALG_1:def 10
for x being set st x in dom IT holds
IT . x is Universal_Algebra;
end;
:: deftheorem Def10 defines Univ_Alg-yielding PRALG_1:def_10_:_
for IT being Function holds
( IT is Univ_Alg-yielding iff for x being set st x in dom IT holds
IT . x is Universal_Algebra );
definition
let IT be Function;
attrIT is 1-sorted-yielding means :Def11: :: PRALG_1:def 11
for x being set st x in dom IT holds
IT . x is 1-sorted ;
end;
:: deftheorem Def11 defines 1-sorted-yielding PRALG_1:def_11_:_
for IT being Function holds
( IT is 1-sorted-yielding iff for x being set st x in dom IT holds
IT . x is 1-sorted );
registration
cluster Relation-like Function-like Univ_Alg-yielding for set ;
existence
ex b1 being Function st b1 is Univ_Alg-yielding
proof
reconsider f = {} as Function ;
take f ; ::_thesis: f is Univ_Alg-yielding
let x be set ; :: according to PRALG_1:def_10 ::_thesis: ( x in dom f implies f . x is Universal_Algebra )
thus ( x in dom f implies f . x is Universal_Algebra ) ; ::_thesis: verum
end;
end;
registration
cluster Relation-like Function-like Univ_Alg-yielding -> 1-sorted-yielding for set ;
coherence
for b1 being Function st b1 is Univ_Alg-yielding holds
b1 is 1-sorted-yielding
proof
let F be Function; ::_thesis: ( F is Univ_Alg-yielding implies F is 1-sorted-yielding )
assume F is Univ_Alg-yielding ; ::_thesis: F is 1-sorted-yielding
then for x being set st x in dom F holds
F . x is 1-sorted by Def10;
hence F is 1-sorted-yielding by Def11; ::_thesis: verum
end;
end;
registration
let I be set ;
cluster Relation-like I -defined Function-like total 1-sorted-yielding for set ;
existence
ex b1 being ManySortedSet of I st b1 is 1-sorted-yielding
proof
set A = the 1-sorted ;
set f = I --> the 1-sorted ;
A1: dom (I --> the 1-sorted ) = I by FUNCOP_1:13;
reconsider f = I --> the 1-sorted as ManySortedSet of I ;
take f ; ::_thesis: f is 1-sorted-yielding
for i being set st i in dom f holds
f . i is 1-sorted by A1, FUNCOP_1:7;
hence f is 1-sorted-yielding by Def11; ::_thesis: verum
end;
end;
definition
let IT be Function;
attrIT is equal-signature means :Def12: :: PRALG_1:def 12
for x, y being set st x in dom IT & y in dom IT holds
for U1, U2 being Universal_Algebra st U1 = IT . x & U2 = IT . y holds
signature U1 = signature U2;
end;
:: deftheorem Def12 defines equal-signature PRALG_1:def_12_:_
for IT being Function holds
( IT is equal-signature iff for x, y being set st x in dom IT & y in dom IT holds
for U1, U2 being Universal_Algebra st U1 = IT . x & U2 = IT . y holds
signature U1 = signature U2 );
registration
let J be non empty set ;
cluster Relation-like J -defined Function-like non empty total Univ_Alg-yielding equal-signature for set ;
existence
ex b1 being ManySortedSet of J st
( b1 is equal-signature & b1 is Univ_Alg-yielding )
proof
set U1 = the Universal_Algebra;
set f = J --> the Universal_Algebra;
A1: dom (J --> the Universal_Algebra) = J by FUNCOP_1:13;
reconsider f = J --> the Universal_Algebra as ManySortedSet of J ;
take f ; ::_thesis: ( f is equal-signature & f is Univ_Alg-yielding )
for x, y being set st x in dom f & y in dom f holds
for U1, U2 being Universal_Algebra st U1 = f . x & U2 = f . y holds
signature U1 = signature U2
proof
let x, y be set ; ::_thesis: ( x in dom f & y in dom f implies for U1, U2 being Universal_Algebra st U1 = f . x & U2 = f . y holds
signature U1 = signature U2 )
assume that
A2: x in dom f and
A3: y in dom f ; ::_thesis: for U1, U2 being Universal_Algebra st U1 = f . x & U2 = f . y holds
signature U1 = signature U2
let U2, U3 be Universal_Algebra; ::_thesis: ( U2 = f . x & U3 = f . y implies signature U2 = signature U3 )
assume A4: ( U2 = f . x & U3 = f . y ) ; ::_thesis: signature U2 = signature U3
f . x = the Universal_Algebra by A1, A2, FUNCOP_1:7;
hence signature U2 = signature U3 by A1, A3, A4, FUNCOP_1:7; ::_thesis: verum
end;
hence f is equal-signature by Def12; ::_thesis: f is Univ_Alg-yielding
for x being set st x in dom f holds
f . x is Universal_Algebra by A1, FUNCOP_1:7;
hence f is Univ_Alg-yielding by Def10; ::_thesis: verum
end;
end;
definition
let J be non empty set ;
let A be 1-sorted-yielding ManySortedSet of J;
let j be Element of J;
:: original: .
redefine funcA . j -> 1-sorted ;
coherence
A . j is 1-sorted
proof
dom A = J by PARTFUN1:def_2;
hence A . j is 1-sorted by Def11; ::_thesis: verum
end;
end;
definition
let J be non empty set ;
let A be Univ_Alg-yielding ManySortedSet of J;
let j be Element of J;
:: original: .
redefine funcA . j -> Universal_Algebra;
coherence
A . j is Universal_Algebra
proof
dom A = J by PARTFUN1:def_2;
hence A . j is Universal_Algebra by Def10; ::_thesis: verum
end;
end;
definition
let J be set ;
let A be 1-sorted-yielding ManySortedSet of J;
func Carrier A -> ManySortedSet of J means :Def13: :: PRALG_1:def 13
for j being set st j in J holds
ex R being 1-sorted st
( R = A . j & it . j = the carrier of R );
existence
ex b1 being ManySortedSet of J st
for j being set st j in J holds
ex R being 1-sorted st
( R = A . j & b1 . j = the carrier of R )
proof
defpred S1[ set , set ] means ex R being 1-sorted st
( R = A . $1 & $2 = the carrier of R );
A1: for i being set st i in J holds
ex j being set st S1[i,j]
proof
let i be set ; ::_thesis: ( i in J implies ex j being set st S1[i,j] )
assume A2: i in J ; ::_thesis: ex j being set st S1[i,j]
then reconsider J = J as non empty set ;
reconsider i9 = i as Element of J by A2;
reconsider B = A as 1-sorted-yielding ManySortedSet of J ;
take the carrier of (B . i9) ; ::_thesis: S1[i, the carrier of (B . i9)]
take B . i9 ; ::_thesis: ( B . i9 = A . i & the carrier of (B . i9) = the carrier of (B . i9) )
thus ( B . i9 = A . i & the carrier of (B . i9) = the carrier of (B . i9) ) ; ::_thesis: verum
end;
consider M being Function such that
A3: dom M = J and
A4: for i being set st i in J holds
S1[i,M . i] from CLASSES1:sch_1(A1);
reconsider M = M as ManySortedSet of J by A3, PARTFUN1:def_2, RELAT_1:def_18;
take M ; ::_thesis: for j being set st j in J holds
ex R being 1-sorted st
( R = A . j & M . j = the carrier of R )
thus for j being set st j in J holds
ex R being 1-sorted st
( R = A . j & M . j = the carrier of R ) by A4; ::_thesis: verum
end;
uniqueness
for b1, b2 being ManySortedSet of J st ( for j being set st j in J holds
ex R being 1-sorted st
( R = A . j & b1 . j = the carrier of R ) ) & ( for j being set st j in J holds
ex R being 1-sorted st
( R = A . j & b2 . j = the carrier of R ) ) holds
b1 = b2
proof
let X, Y be ManySortedSet of J; ::_thesis: ( ( for j being set st j in J holds
ex R being 1-sorted st
( R = A . j & X . j = the carrier of R ) ) & ( for j being set st j in J holds
ex R being 1-sorted st
( R = A . j & Y . j = the carrier of R ) ) implies X = Y )
assume A5: ( ( for j being set st j in J holds
ex R being 1-sorted st
( R = A . j & X . j = the carrier of R ) ) & ( for j being set st j in J holds
ex R being 1-sorted st
( R = A . j & Y . j = the carrier of R ) ) ) ; ::_thesis: X = Y
for i being set st i in J holds
X . i = Y . i
proof
let i be set ; ::_thesis: ( i in J implies X . i = Y . i )
assume i in J ; ::_thesis: X . i = Y . i
then ( ex R being 1-sorted st
( R = A . i & X . i = the carrier of R ) & ex R being 1-sorted st
( R = A . i & Y . i = the carrier of R ) ) by A5;
hence X . i = Y . i ; ::_thesis: verum
end;
hence X = Y by PBOOLE:3; ::_thesis: verum
end;
end;
:: deftheorem Def13 defines Carrier PRALG_1:def_13_:_
for J being set
for A being 1-sorted-yielding ManySortedSet of J
for b3 being ManySortedSet of J holds
( b3 = Carrier A iff for j being set st j in J holds
ex R being 1-sorted st
( R = A . j & b3 . j = the carrier of R ) );
registration
let J be non empty set ;
let A be Univ_Alg-yielding ManySortedSet of J;
cluster Carrier A -> V2() ;
coherence
Carrier A is non-empty
proof
let i be set ; :: according to PBOOLE:def_13 ::_thesis: ( not i in J or not (Carrier A) . i is empty )
assume A1: i in J ; ::_thesis: not (Carrier A) . i is empty
then consider R being 1-sorted such that
A2: R = A . i and
A3: (Carrier A) . i = the carrier of R by Def13;
dom A = J by PARTFUN1:def_2;
then R is Universal_Algebra by A1, A2, Def10;
hence not (Carrier A) . i is empty by A3; ::_thesis: verum
end;
end;
definition
let J be non empty set ;
let A be Univ_Alg-yielding equal-signature ManySortedSet of J;
func ComSign A -> FinSequence of NAT means :Def14: :: PRALG_1:def 14
for j being Element of J holds it = signature (A . j);
existence
ex b1 being FinSequence of NAT st
for j being Element of J holds b1 = signature (A . j)
proof
set j = the Element of J;
reconsider U0 = A . the Element of J as Universal_Algebra ;
take signature U0 ; ::_thesis: for j being Element of J holds signature U0 = signature (A . j)
let j1 be Element of J; ::_thesis: signature U0 = signature (A . j1)
dom A = J by PARTFUN1:def_2;
hence signature U0 = signature (A . j1) by Def12; ::_thesis: verum
end;
uniqueness
for b1, b2 being FinSequence of NAT st ( for j being Element of J holds b1 = signature (A . j) ) & ( for j being Element of J holds b2 = signature (A . j) ) holds
b1 = b2
proof
set j = the Element of J;
let X, Y be FinSequence of NAT ; ::_thesis: ( ( for j being Element of J holds X = signature (A . j) ) & ( for j being Element of J holds Y = signature (A . j) ) implies X = Y )
assume that
A1: for j being Element of J holds X = signature (A . j) and
A2: for j being Element of J holds Y = signature (A . j) ; ::_thesis: X = Y
reconsider U0 = A . the Element of J as Universal_Algebra ;
X = signature U0 by A1;
hence X = Y by A2; ::_thesis: verum
end;
end;
:: deftheorem Def14 defines ComSign PRALG_1:def_14_:_
for J being non empty set
for A being Univ_Alg-yielding equal-signature ManySortedSet of J
for b3 being FinSequence of NAT holds
( b3 = ComSign A iff for j being Element of J holds b3 = signature (A . j) );
registration
let J be non empty set ;
let B be V2() ManySortedSet of J;
cluster product B -> non empty ;
coherence
not product B is empty ;
end;
definition
let J be non empty set ;
let B be V2() ManySortedSet of J;
mode ManySortedOperation of B -> ManySortedFunction of J means :Def15: :: PRALG_1:def 15
for j being Element of J holds it . j is non empty homogeneous quasi_total PartFunc of ((B . j) *),(B . j);
existence
ex b1 being ManySortedFunction of J st
for j being Element of J holds b1 . j is non empty homogeneous quasi_total PartFunc of ((B . j) *),(B . j)
proof
defpred S1[ set , set ] means $2 in B . $1;
A1: for x being set st x in J holds
ex y being set st S1[x,y] by XBOOLE_0:def_1;
consider f being Function such that
A2: ( dom f = J & ( for x being set st x in J holds
S1[x,f . x] ) ) from CLASSES1:sch_1(A1);
deffunc H1( set ) -> set = (<*> (B . $1)) .--> (f . $1);
consider F being Function such that
A3: ( dom F = J & ( for x being set st x in J holds
F . x = H1(x) ) ) from FUNCT_1:sch_3();
reconsider F = F as ManySortedSet of J by A3, 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 F . x = (<*> (B . x)) .--> (f . x) by A3;
hence F . x is Function ; ::_thesis: verum
end;
then reconsider F = F as ManySortedFunction of J by FUNCOP_1:def_6;
take F ; ::_thesis: for j being Element of J holds F . j is non empty homogeneous quasi_total PartFunc of ((B . j) *),(B . j)
let j be Element of J; ::_thesis: F . j is non empty homogeneous quasi_total PartFunc of ((B . j) *),(B . j)
reconsider b = f . j as Element of B . j by A2;
F . j = (<*> (B . j)) .--> b by A3;
hence F . j is non empty homogeneous quasi_total PartFunc of ((B . j) *),(B . j) by MARGREL1:18; ::_thesis: verum
end;
end;
:: deftheorem Def15 defines ManySortedOperation PRALG_1:def_15_:_
for J being non empty set
for B being V2() ManySortedSet of J
for b3 being ManySortedFunction of J holds
( b3 is ManySortedOperation of B iff for j being Element of J holds b3 . j is non empty homogeneous quasi_total PartFunc of ((B . j) *),(B . j) );
definition
let J be non empty set ;
let B be V2() ManySortedSet of J;
let O be ManySortedOperation of B;
let j be Element of J;
:: original: .
redefine funcO . j -> non empty homogeneous quasi_total PartFunc of ((B . j) *),(B . j);
coherence
O . j is non empty homogeneous quasi_total PartFunc of ((B . j) *),(B . j) by Def15;
end;
definition
let IT be Function;
attrIT is equal-arity means :Def16: :: PRALG_1:def 16
for x, y being set st x in dom IT & y in dom IT holds
for f, g being Function st IT . x = f & IT . y = g holds
for n, m being Nat
for X, Y being non empty set st dom f = n -tuples_on X & dom g = m -tuples_on Y holds
for o1 being non empty homogeneous quasi_total PartFunc of (X *),X
for o2 being non empty homogeneous quasi_total PartFunc of (Y *),Y st f = o1 & g = o2 holds
arity o1 = arity o2;
end;
:: deftheorem Def16 defines equal-arity PRALG_1:def_16_:_
for IT being Function holds
( IT is equal-arity iff for x, y being set st x in dom IT & y in dom IT holds
for f, g being Function st IT . x = f & IT . y = g holds
for n, m being Nat
for X, Y being non empty set st dom f = n -tuples_on X & dom g = m -tuples_on Y holds
for o1 being non empty homogeneous quasi_total PartFunc of (X *),X
for o2 being non empty homogeneous quasi_total PartFunc of (Y *),Y st f = o1 & g = o2 holds
arity o1 = arity o2 );
registration
let J be non empty set ;
let B be V2() ManySortedSet of J;
cluster Relation-like J -defined Function-like non empty total Function-yielding V45() equal-arity for ManySortedOperation of B;
existence
ex b1 being ManySortedOperation of B st b1 is equal-arity
proof
defpred S1[ set , set ] means B in B . J;
A1: for x being set st x in J holds
ex y being set st S1[x,y] by XBOOLE_0:def_1;
consider f being Function such that
A2: ( dom f = J & ( for x being set st x in J holds
S1[x,f . x] ) ) from CLASSES1:sch_1(A1);
deffunc H1( set ) -> set = (<*> (B . J)) .--> (f . J);
consider F being Function such that
A3: ( dom F = J & ( for x being set st x in J holds
F . x = H1(x) ) ) from FUNCT_1:sch_3();
reconsider F = F as ManySortedSet of J by A3, 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 F . x = (<*> (B . x)) .--> (f . x) by A3;
hence F . x is Function ; ::_thesis: verum
end;
then reconsider F = F as ManySortedFunction of J by FUNCOP_1:def_6;
now__::_thesis:_for_j_being_Element_of_J_holds_F_._j_is_non_empty_homogeneous_quasi_total_PartFunc_of_((B_._j)_*),(B_._j)
let j be Element of J; ::_thesis: F . j is non empty homogeneous quasi_total PartFunc of ((B . j) *),(B . j)
reconsider b = f . j as Element of B . j by A2;
F . j = (<*> (B . j)) .--> b by A3;
hence F . j is non empty homogeneous quasi_total PartFunc of ((B . j) *),(B . j) by MARGREL1:18; ::_thesis: verum
end;
then reconsider F = F as ManySortedOperation of B by Def15;
take F ; ::_thesis: F is equal-arity
for x, y being set st x in dom F & y in dom F holds
for f, g being Function st F . x = f & F . y = g holds
for n, m being Nat
for X, Y being non empty set st dom f = n -tuples_on X & dom g = m -tuples_on Y holds
for o1 being non empty homogeneous quasi_total PartFunc of (X *),X
for o2 being non empty homogeneous quasi_total PartFunc of (Y *),Y st f = o1 & g = o2 holds
arity o1 = arity o2
proof
let x, y be set ; ::_thesis: ( x in dom F & y in dom F implies for f, g being Function st F . x = f & F . y = g holds
for n, m being Nat
for X, Y being non empty set st dom f = n -tuples_on X & dom g = m -tuples_on Y holds
for o1 being non empty homogeneous quasi_total PartFunc of (X *),X
for o2 being non empty homogeneous quasi_total PartFunc of (Y *),Y st f = o1 & g = o2 holds
arity o1 = arity o2 )
assume that
A4: x in dom F and
A5: y in dom F ; ::_thesis: for f, g being Function st F . x = f & F . y = g holds
for n, m being Nat
for X, Y being non empty set st dom f = n -tuples_on X & dom g = m -tuples_on Y holds
for o1 being non empty homogeneous quasi_total PartFunc of (X *),X
for o2 being non empty homogeneous quasi_total PartFunc of (Y *),Y st f = o1 & g = o2 holds
arity o1 = arity o2
reconsider x1 = x, y1 = y as Element of J by A3, A4, A5;
let g, h be Function; ::_thesis: ( F . x = g & F . y = h implies for n, m being Nat
for X, Y being non empty set st dom g = n -tuples_on X & dom h = m -tuples_on Y holds
for o1 being non empty homogeneous quasi_total PartFunc of (X *),X
for o2 being non empty homogeneous quasi_total PartFunc of (Y *),Y st g = o1 & h = o2 holds
arity o1 = arity o2 )
assume that
A6: F . x = g and
A7: F . y = h ; ::_thesis: for n, m being Nat
for X, Y being non empty set st dom g = n -tuples_on X & dom h = m -tuples_on Y holds
for o1 being non empty homogeneous quasi_total PartFunc of (X *),X
for o2 being non empty homogeneous quasi_total PartFunc of (Y *),Y st g = o1 & h = o2 holds
arity o1 = arity o2
reconsider fx = f . x1 as Element of B . x1 by A2;
let n, m be Nat; ::_thesis: for X, Y being non empty set st dom g = n -tuples_on X & dom h = m -tuples_on Y holds
for o1 being non empty homogeneous quasi_total PartFunc of (X *),X
for o2 being non empty homogeneous quasi_total PartFunc of (Y *),Y st g = o1 & h = o2 holds
arity o1 = arity o2
let X, Y be non empty set ; ::_thesis: ( dom g = n -tuples_on X & dom h = m -tuples_on Y implies for o1 being non empty homogeneous quasi_total PartFunc of (X *),X
for o2 being non empty homogeneous quasi_total PartFunc of (Y *),Y st g = o1 & h = o2 holds
arity o1 = arity o2 )
assume that
dom g = n -tuples_on X and
dom h = m -tuples_on Y ; ::_thesis: for o1 being non empty homogeneous quasi_total PartFunc of (X *),X
for o2 being non empty homogeneous quasi_total PartFunc of (Y *),Y st g = o1 & h = o2 holds
arity o1 = arity o2
let o1 be non empty homogeneous quasi_total PartFunc of (X *),X; ::_thesis: for o2 being non empty homogeneous quasi_total PartFunc of (Y *),Y st g = o1 & h = o2 holds
arity o1 = arity o2
let o2 be non empty homogeneous quasi_total PartFunc of (Y *),Y; ::_thesis: ( g = o1 & h = o2 implies arity o1 = arity o2 )
assume that
A8: g = o1 and
A9: h = o2 ; ::_thesis: arity o1 = arity o2
reconsider o1x = (<*> (B . x1)) .--> fx as non empty homogeneous quasi_total PartFunc of ((B . x1) *),(B . x1) by MARGREL1:18;
A10: dom o1x = {({} (B . x1))} by FUNCOP_1:13;
consider p1 being set such that
A11: p1 in dom o1 by XBOOLE_0:def_1;
dom o1 c= X * by RELAT_1:def_18;
then reconsider p1 = p1 as Element of X * by A11;
o1 = (<*> (B . x)) .--> (f . x) by A3, A4, A6, A8;
then p1 = <*> (B . x1) by A10, A11, TARSKI:def_1;
then len p1 = 0 ;
then A12: arity o1 = 0 by A11, MARGREL1:def_25;
reconsider fy = f . y1 as Element of B . y1 by A2;
reconsider o2y = (<*> (B . y1)) .--> fy as non empty homogeneous quasi_total PartFunc of ((B . y1) *),(B . y1) by MARGREL1:18;
A13: dom o2y = {({} (B . y1))} by FUNCOP_1:13;
consider p2 being set such that
A14: p2 in dom o2 by XBOOLE_0:def_1;
dom o2 c= Y * by RELAT_1:def_18;
then reconsider p2 = p2 as Element of Y * by A14;
o2 = (<*> (B . y)) .--> (f . y) by A3, A5, A7, A9;
then p2 = <*> (B . y1) by A13, A14, TARSKI:def_1;
then len p2 = 0 ;
hence arity o1 = arity o2 by A12, A14, MARGREL1:def_25; ::_thesis: verum
end;
hence F is equal-arity by Def16; ::_thesis: verum
end;
end;
theorem Th11: :: PRALG_1:11
for J being non empty set
for B being V2() ManySortedSet of J
for O being ManySortedOperation of B holds
( O is equal-arity iff for i, j being Element of J holds arity (O . i) = arity (O . j) )
proof
let J be non empty set ; ::_thesis: for B being V2() ManySortedSet of J
for O being ManySortedOperation of B holds
( O is equal-arity iff for i, j being Element of J holds arity (O . i) = arity (O . j) )
let B be V2() ManySortedSet of J; ::_thesis: for O being ManySortedOperation of B holds
( O is equal-arity iff for i, j being Element of J holds arity (O . i) = arity (O . j) )
let O be ManySortedOperation of B; ::_thesis: ( O is equal-arity iff for i, j being Element of J holds arity (O . i) = arity (O . j) )
thus ( O is equal-arity implies for i, j being Element of J holds arity (O . i) = arity (O . j) ) ::_thesis: ( ( for i, j being Element of J holds arity (O . i) = arity (O . j) ) implies O is equal-arity )
proof
assume A1: O is equal-arity ; ::_thesis: for i, j being Element of J holds arity (O . i) = arity (O . j)
let i, j be Element of J; ::_thesis: arity (O . i) = arity (O . j)
A2: dom (O . j) = (arity (O . j)) -tuples_on (B . j) by MARGREL1:22;
( dom O = J & dom (O . i) = (arity (O . i)) -tuples_on (B . i) ) by MARGREL1:22, PARTFUN1:def_2;
hence arity (O . i) = arity (O . j) by A1, A2, Def16; ::_thesis: verum
end;
assume A3: for i, j being Element of J holds arity (O . i) = arity (O . j) ; ::_thesis: O is equal-arity
let x, y be set ; :: according to PRALG_1:def_16 ::_thesis: ( x in dom O & y in dom O implies for f, g being Function st O . x = f & O . y = g holds
for n, m being Nat
for X, Y being non empty set st dom f = n -tuples_on X & dom g = m -tuples_on Y holds
for o1 being non empty homogeneous quasi_total PartFunc of (X *),X
for o2 being non empty homogeneous quasi_total PartFunc of (Y *),Y st f = o1 & g = o2 holds
arity o1 = arity o2 )
assume ( x in dom O & y in dom O ) ; ::_thesis: for f, g being Function st O . x = f & O . y = g holds
for n, m being Nat
for X, Y being non empty set st dom f = n -tuples_on X & dom g = m -tuples_on Y holds
for o1 being non empty homogeneous quasi_total PartFunc of (X *),X
for o2 being non empty homogeneous quasi_total PartFunc of (Y *),Y st f = o1 & g = o2 holds
arity o1 = arity o2
then reconsider x1 = x, y1 = y as Element of J by PARTFUN1:def_2;
let f, g be Function; ::_thesis: ( O . x = f & O . y = g implies for n, m being Nat
for X, Y being non empty set st dom f = n -tuples_on X & dom g = m -tuples_on Y holds
for o1 being non empty homogeneous quasi_total PartFunc of (X *),X
for o2 being non empty homogeneous quasi_total PartFunc of (Y *),Y st f = o1 & g = o2 holds
arity o1 = arity o2 )
assume that
A4: O . x = f and
A5: O . y = g ; ::_thesis: for n, m being Nat
for X, Y being non empty set st dom f = n -tuples_on X & dom g = m -tuples_on Y holds
for o1 being non empty homogeneous quasi_total PartFunc of (X *),X
for o2 being non empty homogeneous quasi_total PartFunc of (Y *),Y st f = o1 & g = o2 holds
arity o1 = arity o2
arity (O . x1) = arity (O . y1) by A3;
then A6: dom g = (arity (O . x1)) -tuples_on (B . y1) by A5, MARGREL1:22;
let n, m be Nat; ::_thesis: for X, Y being non empty set st dom f = n -tuples_on X & dom g = m -tuples_on Y holds
for o1 being non empty homogeneous quasi_total PartFunc of (X *),X
for o2 being non empty homogeneous quasi_total PartFunc of (Y *),Y st f = o1 & g = o2 holds
arity o1 = arity o2
let X, Y be non empty set ; ::_thesis: ( dom f = n -tuples_on X & dom g = m -tuples_on Y implies for o1 being non empty homogeneous quasi_total PartFunc of (X *),X
for o2 being non empty homogeneous quasi_total PartFunc of (Y *),Y st f = o1 & g = o2 holds
arity o1 = arity o2 )
assume that
A7: dom f = n -tuples_on X and
A8: dom g = m -tuples_on Y ; ::_thesis: for o1 being non empty homogeneous quasi_total PartFunc of (X *),X
for o2 being non empty homogeneous quasi_total PartFunc of (Y *),Y st f = o1 & g = o2 holds
arity o1 = arity o2
dom f = (arity (O . x1)) -tuples_on (B . x1) by A4, MARGREL1:22;
then A9: n = arity (O . x1) by A7, FINSEQ_2:110;
set p = the Element of n -tuples_on X;
set q = the Element of m -tuples_on Y;
let o1 be non empty homogeneous quasi_total PartFunc of (X *),X; ::_thesis: for o2 being non empty homogeneous quasi_total PartFunc of (Y *),Y st f = o1 & g = o2 holds
arity o1 = arity o2
let o2 be non empty homogeneous quasi_total PartFunc of (Y *),Y; ::_thesis: ( f = o1 & g = o2 implies arity o1 = arity o2 )
assume that
A10: f = o1 and
A11: g = o2 ; ::_thesis: arity o1 = arity o2
A12: arity o2 = len the Element of m -tuples_on Y by A8, A11, MARGREL1:def_25
.= m by CARD_1:def_7 ;
arity o1 = len the Element of n -tuples_on X by A7, A10, MARGREL1:def_25
.= n by CARD_1:def_7 ;
hence arity o1 = arity o2 by A8, A6, A9, A12, FINSEQ_2:110; ::_thesis: verum
end;
definition
let F be Function-yielding Function;
let f be Function;
funcF .. f -> Function means :Def17: :: PRALG_1:def 17
( dom it = dom F & ( for x being set st x in dom F holds
it . x = (F . x) . (f . x) ) );
existence
ex b1 being Function st
( dom b1 = dom F & ( for x being set st x in dom F holds
b1 . x = (F . x) . (f . x) ) )
proof
set I = dom F;
defpred S1[ set , set ] means $2 = (F . $1) . (f . $1);
A1: for i being set st i in dom F holds
ex y being set st S1[i,y] ;
consider F being Function such that
A2: ( dom F = dom F & ( for i being set st i in dom F holds
S1[i,F . i] ) ) from CLASSES1:sch_1(A1);
take F ; ::_thesis: ( dom F = dom F & ( for x being set st x in dom F holds
F . x = (F . x) . (f . x) ) )
thus ( dom F = dom F & ( for x being set st x in dom F holds
F . x = (F . x) . (f . x) ) ) by A2; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function st dom b1 = dom F & ( for x being set st x in dom F holds
b1 . x = (F . x) . (f . x) ) & dom b2 = dom F & ( for x being set st x in dom F holds
b2 . x = (F . x) . (f . x) ) holds
b1 = b2
proof
let m, n be Function; ::_thesis: ( dom m = dom F & ( for x being set st x in dom F holds
m . x = (F . x) . (f . x) ) & dom n = dom F & ( for x being set st x in dom F holds
n . x = (F . x) . (f . x) ) implies m = n )
assume that
A3: dom m = dom F and
A4: for x being set st x in dom F holds
m . x = (F . x) . (f . x) and
A5: dom n = dom F and
A6: for x being set st x in dom F holds
n . x = (F . x) . (f . x) ; ::_thesis: m = n
for x being set st x in dom m holds
m . x = n . x
proof
let x be set ; ::_thesis: ( x in dom m implies m . x = n . x )
consider g being set such that
A7: g = F . x ;
reconsider g = g as Function by A7;
assume A8: x in dom m ; ::_thesis: m . x = n . x
then m . x = g . (f . x) by A3, A4, A7;
hence m . x = n . x by A3, A6, A8, A7; ::_thesis: verum
end;
hence m = n by A3, A5, FUNCT_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def17 defines .. PRALG_1:def_17_:_
for F being Function-yielding Function
for f, b3 being Function holds
( b3 = F .. f iff ( dom b3 = dom F & ( for x being set st x in dom F holds
b3 . x = (F . x) . (f . x) ) ) );
registration
let I be set ;
let f be ManySortedFunction of I;
let x be ManySortedSet of I;
clusterf .. x -> I -defined ;
coherence
f .. x is I -defined
proof
dom (f .. x) = dom f by Def17
.= I by PARTFUN1:def_2 ;
hence f .. x is I -defined by RELAT_1:def_18; ::_thesis: verum
end;
end;
registration
let I be set ;
let f be ManySortedFunction of I;
let x be ManySortedSet of I;
clusterf .. x -> I -defined total for I -defined Function;
coherence
for b1 being I -defined Function st b1 = f .. x holds
b1 is total
proof
dom (f .. x) = dom f by Def17
.= I by PARTFUN1:def_2 ;
hence for b1 being I -defined Function st b1 = f .. x holds
b1 is total by PARTFUN1:def_2; ::_thesis: verum
end;
end;
definition
let I be set ;
let f be ManySortedFunction of I;
let x be ManySortedSet of I;
:: original: ..
redefine funcf .. x -> Function means :Def18: :: PRALG_1:def 18
( dom it = I & ( for i being set st i in I holds
for g being Function st g = f . i holds
it . i = g . (x . i) ) );
compatibility
for b1 being Function holds
( b1 = f .. x iff ( dom b1 = I & ( for i being set st i in I holds
for g being Function st g = f . i holds
b1 . i = g . (x . i) ) ) )
proof
let M be Function; ::_thesis: ( M = f .. x iff ( dom M = I & ( for i being set st i in I holds
for g being Function st g = f . i holds
M . i = g . (x . i) ) ) )
hereby ::_thesis: ( dom M = I & ( for i being set st i in I holds
for g being Function st g = f . i holds
M . i = g . (x . i) ) implies M = f .. x )
assume A1: M = f .. x ; ::_thesis: ( dom M = I & ( for i being set st i in I holds
for g being Function st g = f . i holds
M . i = g . (x . i) ) )
hence A2: dom M = I by PARTFUN1:def_2; ::_thesis: for i being set st i in I holds
for g being Function st g = f . i holds
M . i = g . (x . i)
dom M = dom f by A1, Def17;
hence for i being set st i in I holds
for g being Function st g = f . i holds
M . i = g . (x . i) by A1, A2, Def17; ::_thesis: verum
end;
assume that
A3: dom M = I and
A4: for i being set st i in I holds
for g being Function st g = f . i holds
M . i = g . (x . i) ; ::_thesis: M = f .. x
A5: dom f = I by PARTFUN1:def_2;
then for i being set st i in dom f holds
M . i = (f . i) . (x . i) by A4;
hence M = f .. x by A3, A5, Def17; ::_thesis: verum
end;
end;
:: deftheorem Def18 defines .. PRALG_1:def_18_:_
for I being set
for f being ManySortedFunction of I
for x being ManySortedSet of I
for b4 being Function holds
( b4 = f .. x iff ( dom b4 = I & ( for i being set st i in I holds
for g being Function st g = f . i holds
b4 . i = g . (x . i) ) ) );
registration
let J be non empty set ;
let B be V2() ManySortedSet of J;
let p be FinSequence of product B;
cluster uncurry p -> [:(dom p),J:] -defined ;
coherence
uncurry p is [:(dom p),J:] -defined
proof
now__::_thesis:_uncurry_p_is_[:(dom_p),J:]_-defined
set j = the Element of J;
dom B = J by PARTFUN1:def_2;
then B . the Element of J in rng B by FUNCT_1:def_3;
then reconsider S = union (rng B) as non empty set by XBOOLE_1:3, ZFMISC_1:74;
rng p c= Funcs (J,S)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng p or x in Funcs (J,S) )
A1: rng p c= product B by FINSEQ_1:def_4;
assume x in rng p ; ::_thesis: x in Funcs (J,S)
then consider f being Function such that
A2: x = f and
A3: dom f = dom B and
A4: for y being set st y in dom B holds
f . y in B . y by A1, CARD_3:def_5;
A5: rng f c= S
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng f or z in S )
assume z in rng f ; ::_thesis: z in S
then consider y being set such that
A6: y in dom f and
A7: z = f . y by FUNCT_1:def_3;
B . y in rng B by A3, A6, FUNCT_1:def_3;
then A8: B . y c= union (rng B) by ZFMISC_1:74;
z in B . y by A3, A4, A6, A7;
hence z in S by A8; ::_thesis: verum
end;
dom B = J by PARTFUN1:def_2;
hence x in Funcs (J,S) by A2, A3, A5, FUNCT_2:def_2; ::_thesis: verum
end;
then dom (uncurry p) = [:(dom p),J:] by FUNCT_5:26;
hence uncurry p is [:(dom p),J:] -defined by RELAT_1:def_18; ::_thesis: verum
end;
hence uncurry p is [:(dom p),J:] -defined ; ::_thesis: verum
end;
end;
registration
let J be non empty set ;
let B be V2() ManySortedSet of J;
let p be FinSequence of product B;
cluster uncurry p -> [:(dom p),J:] -defined total for [:(dom p),J:] -defined Function;
coherence
for b1 being [:(dom p),J:] -defined Function st b1 = uncurry p holds
b1 is total
proof
now__::_thesis:_for_b1_being_[:(dom_p),J:]_-defined_Function_st_b1_=_uncurry_p_holds_
b1_is_total
set j = the Element of J;
dom B = J by PARTFUN1:def_2;
then B . the Element of J in rng B by FUNCT_1:def_3;
then reconsider S = union (rng B) as non empty set by XBOOLE_1:3, ZFMISC_1:74;
rng p c= Funcs (J,S)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng p or x in Funcs (J,S) )
A1: rng p c= product B by FINSEQ_1:def_4;
assume x in rng p ; ::_thesis: x in Funcs (J,S)
then consider f being Function such that
A2: x = f and
A3: dom f = dom B and
A4: for y being set st y in dom B holds
f . y in B . y by A1, CARD_3:def_5;
A5: rng f c= S
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng f or z in S )
assume z in rng f ; ::_thesis: z in S
then consider y being set such that
A6: y in dom f and
A7: z = f . y by FUNCT_1:def_3;
B . y in rng B by A3, A6, FUNCT_1:def_3;
then A8: B . y c= union (rng B) by ZFMISC_1:74;
z in B . y by A3, A4, A6, A7;
hence z in S by A8; ::_thesis: verum
end;
dom B = J by PARTFUN1:def_2;
hence x in Funcs (J,S) by A2, A3, A5, FUNCT_2:def_2; ::_thesis: verum
end;
then dom (uncurry p) = [:(dom p),J:] by FUNCT_5:26;
hence for b1 being [:(dom p),J:] -defined Function st b1 = uncurry p holds
b1 is total by PARTFUN1:def_2; ::_thesis: verum
end;
hence for b1 being [:(dom p),J:] -defined Function st b1 = uncurry p holds
b1 is total ; ::_thesis: verum
end;
end;
registration
let I, J be set ;
let X be ManySortedSet of [:I,J:];
cluster ~ X -> [:J,I:] -defined ;
coherence
~ X is [:J,I:] -defined
proof
dom X = [:I,J:] by PARTFUN1:def_2;
then dom (~ X) = [:J,I:] by FUNCT_4:46;
hence ~ X is [:J,I:] -defined by RELAT_1:def_18; ::_thesis: verum
end;
end;
registration
let I, J be set ;
let X be ManySortedSet of [:I,J:];
cluster ~ X -> [:J,I:] -defined total for [:J,I:] -defined Function;
coherence
for b1 being [:J,I:] -defined Function st b1 = ~ X holds
b1 is total
proof
dom X = [:I,J:] by PARTFUN1:def_2;
then dom (~ X) = [:J,I:] by FUNCT_4:46;
hence for b1 being [:J,I:] -defined Function st b1 = ~ X holds
b1 is total by PARTFUN1:def_2; ::_thesis: verum
end;
end;
registration
let X be set ;
let Y be non empty set ;
let f be ManySortedSet of [:X,Y:];
cluster curry f -> X -defined ;
coherence
curry f is X -defined
proof
set a = curry f;
( dom f = [:X,Y:] & dom (curry f) = proj1 (dom f) ) by FUNCT_5:def_1, PARTFUN1:def_2;
then dom (curry f) = X by FUNCT_5:9;
hence curry f is X -defined by RELAT_1:def_18; ::_thesis: verum
end;
end;
registration
let X be set ;
let Y be non empty set ;
let f be ManySortedSet of [:X,Y:];
cluster curry f -> X -defined total for X -defined Function;
coherence
for b1 being X -defined Function st b1 = curry f holds
b1 is total
proof
set a = curry f;
( dom f = [:X,Y:] & dom (curry f) = proj1 (dom f) ) by FUNCT_5:def_1, PARTFUN1:def_2;
then dom (curry f) = X by FUNCT_5:9;
hence for b1 being X -defined Function st b1 = curry f holds
b1 is total by PARTFUN1:def_2; ::_thesis: verum
end;
end;
definition
let J be non empty set ;
let B be V2() ManySortedSet of J;
let O be equal-arity ManySortedOperation of B;
func ComAr O -> Nat means :Def19: :: PRALG_1:def 19
for j being Element of J holds it = arity (O . j);
existence
ex b1 being Nat st
for j being Element of J holds b1 = arity (O . j)
proof
set i = the Element of J;
take arity (O . the Element of J) ; ::_thesis: for j being Element of J holds arity (O . the Element of J) = arity (O . j)
let j be Element of J; ::_thesis: arity (O . the Element of J) = arity (O . j)
thus arity (O . the Element of J) = arity (O . j) by Th11; ::_thesis: verum
end;
uniqueness
for b1, b2 being Nat st ( for j being Element of J holds b1 = arity (O . j) ) & ( for j being Element of J holds b2 = arity (O . j) ) holds
b1 = b2
proof
set j = the Element of J;
let n, m be Nat; ::_thesis: ( ( for j being Element of J holds n = arity (O . j) ) & ( for j being Element of J holds m = arity (O . j) ) implies n = m )
assume that
A1: for j being Element of J holds n = arity (O . j) and
A2: for j being Element of J holds m = arity (O . j) ; ::_thesis: n = m
n = arity (O . the Element of J) by A1;
hence n = m by A2; ::_thesis: verum
end;
end;
:: deftheorem Def19 defines ComAr PRALG_1:def_19_:_
for J being non empty set
for B being V2() ManySortedSet of J
for O being equal-arity ManySortedOperation of B
for b4 being Nat holds
( b4 = ComAr O iff for j being Element of J holds b4 = arity (O . j) );
definition
let I be set ;
let A be ManySortedSet of I;
func EmptySeq A -> ManySortedSet of I means :Def20: :: PRALG_1:def 20
for i being set st i in I holds
it . i = {} (A . i);
existence
ex b1 being ManySortedSet of I st
for i being set st i in I holds
b1 . i = {} (A . i)
proof
deffunc H1( set ) -> Element of bool (A . $1) = {} (A . $1);
consider f being Function such that
A1: ( dom f = I & ( for x being set st x in I holds
f . x = H1(x) ) ) from FUNCT_1:sch_3();
reconsider f = f as ManySortedSet of I by A1, PARTFUN1:def_2, RELAT_1:def_18;
take f ; ::_thesis: for i being set st i in I holds
f . i = {} (A . i)
thus for i being set st i in I holds
f . i = {} (A . i) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being ManySortedSet of I st ( for i being set st i in I holds
b1 . i = {} (A . i) ) & ( for i being set st i in I holds
b2 . i = {} (A . i) ) holds
b1 = b2
proof
let X, Y be ManySortedSet of I; ::_thesis: ( ( for i being set st i in I holds
X . i = {} (A . i) ) & ( for i being set st i in I holds
Y . i = {} (A . i) ) implies X = Y )
assume that
A2: for i being set st i in I holds
X . i = {} (A . i) and
A3: for i being set st i in I holds
Y . i = {} (A . i) ; ::_thesis: X = Y
for i being set st i in I holds
X . i = Y . i
proof
let i be set ; ::_thesis: ( i in I implies X . i = Y . i )
assume A4: i in I ; ::_thesis: X . i = Y . i
then X . i = {} (A . i) by A2;
hence X . i = Y . i by A3, A4; ::_thesis: verum
end;
hence X = Y by PBOOLE:3; ::_thesis: verum
end;
end;
:: deftheorem Def20 defines EmptySeq PRALG_1:def_20_:_
for I being set
for A, b3 being ManySortedSet of I holds
( b3 = EmptySeq A iff for i being set st i in I holds
b3 . i = {} (A . i) );
definition
let J be non empty set ;
let B be V2() ManySortedSet of J;
let O be equal-arity ManySortedOperation of B;
func[[:O:]] -> non empty homogeneous quasi_total PartFunc of ((product B) *),(product B) means :: PRALG_1:def 21
( dom it = (ComAr O) -tuples_on (product B) & ( for p being Element of (product B) * st p in dom it holds
( ( dom p = {} implies it . p = O .. (EmptySeq B) ) & ( dom p <> {} implies for Z being non empty set
for w being ManySortedSet of [:J,Z:] st Z = dom p & w = ~ (uncurry p) holds
it . p = O .. (curry w) ) ) ) );
existence
ex b1 being non empty homogeneous quasi_total PartFunc of ((product B) *),(product B) st
( dom b1 = (ComAr O) -tuples_on (product B) & ( for p being Element of (product B) * st p in dom b1 holds
( ( dom p = {} implies b1 . p = O .. (EmptySeq B) ) & ( dom p <> {} implies for Z being non empty set
for w being ManySortedSet of [:J,Z:] st Z = dom p & w = ~ (uncurry p) holds
b1 . p = O .. (curry w) ) ) ) )
proof
set pr = product B;
set ca = ComAr O;
set ct = (ComAr O) -tuples_on (product B);
defpred S1[ set , set ] means for p being Element of (product B) * st p = $1 holds
( ( dom p = {} implies $2 = O .. (EmptySeq B) ) & ( dom p <> {} implies for Z being non empty set
for w being ManySortedSet of [:J,Z:] st Z = dom p & w = ~ (uncurry p) holds
$2 = O .. (curry w) ) );
set aa = { q where q is Element of (product B) * : len q = ComAr O } ;
A1: for x being set st x in (ComAr O) -tuples_on (product B) holds
ex y being set st
( y in product B & S1[x,y] )
proof
let x be set ; ::_thesis: ( x in (ComAr O) -tuples_on (product B) implies ex y being set st
( y in product B & S1[x,y] ) )
assume x in (ComAr O) -tuples_on (product B) ; ::_thesis: ex y being set st
( y in product B & S1[x,y] )
then consider w being Element of (product B) * such that
A2: x = w and
A3: len w = ComAr O ;
now__::_thesis:_(_(_dom_w_=_{}_&_ex_y_being_Function_st_
(_y_in_product_B_&_(_for_p_being_Element_of_(product_B)_*_st_p_=_x_holds_
(_(_dom_p_=_{}_implies_y_=_O_.._(EmptySeq_B)_)_&_(_dom_p_<>_{}_implies_for_Z_being_non_empty_set_
for_w_being_ManySortedSet_of_[:J,Z:]_st_Z_=_dom_p_&_w_=_~_(uncurry_p)_holds_
y_=_O_.._(curry_w)_)_)_)_)_)_or_(_dom_w_<>_{}_&_ex_y_being_Function_st_
(_y_in_product_B_&_(_for_l_being_Element_of_(product_B)_*_st_l_=_x_holds_
(_(_dom_l_=_{}_implies_y_=_O_.._(EmptySeq_B)_)_&_(_dom_l_<>_{}_implies_for_Z_being_non_empty_set_
for_w_being_ManySortedSet_of_[:J,Z:]_st_Z_=_dom_l_&_w_=_~_(uncurry_l)_holds_
y_=_O_.._(curry_w)_)_)_)_)_)_)
percases ( dom w = {} or dom w <> {} ) ;
caseA4: dom w = {} ; ::_thesis: ex y being Function st
( y in product B & ( for p being Element of (product B) * st p = x holds
( ( dom p = {} implies y = O .. (EmptySeq B) ) & ( dom p <> {} implies for Z being non empty set
for w being ManySortedSet of [:J,Z:] st Z = dom p & w = ~ (uncurry p) holds
y = O .. (curry w) ) ) ) )
A5: for z being set st z in dom B holds
(O .. (EmptySeq B)) . z in B . z
proof
let z be set ; ::_thesis: ( z in dom B implies (O .. (EmptySeq B)) . z in B . z )
assume z in dom B ; ::_thesis: (O .. (EmptySeq B)) . z in B . z
then reconsider j = z as Element of J by PARTFUN1:def_2;
A6: rng (O . j) c= B . j by RELAT_1:def_19;
w = {} by A4;
then arity (O . j) = 0 by A3, Def19;
then dom (O . j) = 0 -tuples_on (B . j) by MARGREL1:22
.= {(<*> (B . j))} by FINSEQ_2:94 ;
then {} (B . j) in dom (O . j) by TARSKI:def_1;
then A7: (O . j) . ({} (B . j)) in rng (O . j) by FUNCT_1:def_3;
(O .. (EmptySeq B)) . z = (O . j) . ((EmptySeq B) . j) by Def18
.= (O . j) . ({} (B . j)) by Def20 ;
hence (O .. (EmptySeq B)) . z in B . z by A7, A6; ::_thesis: verum
end;
take y = O .. (EmptySeq B); ::_thesis: ( y in product B & ( for p being Element of (product B) * st p = x holds
( ( dom p = {} implies y = O .. (EmptySeq B) ) & ( dom p <> {} implies for Z being non empty set
for w being ManySortedSet of [:J,Z:] st Z = dom p & w = ~ (uncurry p) holds
y = O .. (curry w) ) ) ) )
dom (O .. (EmptySeq B)) = J by PARTFUN1:def_2
.= dom B by PARTFUN1:def_2 ;
hence y in product B by A5, CARD_3:def_5; ::_thesis: for p being Element of (product B) * st p = x holds
( ( dom p = {} implies y = O .. (EmptySeq B) ) & ( dom p <> {} implies for Z being non empty set
for w being ManySortedSet of [:J,Z:] st Z = dom p & w = ~ (uncurry p) holds
y = O .. (curry w) ) )
let p be Element of (product B) * ; ::_thesis: ( p = x implies ( ( dom p = {} implies y = O .. (EmptySeq B) ) & ( dom p <> {} implies for Z being non empty set
for w being ManySortedSet of [:J,Z:] st Z = dom p & w = ~ (uncurry p) holds
y = O .. (curry w) ) ) )
assume p = x ; ::_thesis: ( ( dom p = {} implies y = O .. (EmptySeq B) ) & ( dom p <> {} implies for Z being non empty set
for w being ManySortedSet of [:J,Z:] st Z = dom p & w = ~ (uncurry p) holds
y = O .. (curry w) ) )
hence ( ( dom p = {} implies y = O .. (EmptySeq B) ) & ( dom p <> {} implies for Z being non empty set
for w being ManySortedSet of [:J,Z:] st Z = dom p & w = ~ (uncurry p) holds
y = O .. (curry w) ) ) by A2, A4; ::_thesis: verum
end;
case dom w <> {} ; ::_thesis: ex y being Function st
( y in product B & ( for l being Element of (product B) * st l = x holds
( ( dom l = {} implies y = O .. (EmptySeq B) ) & ( dom l <> {} implies for Z being non empty set
for w being ManySortedSet of [:J,Z:] st Z = dom l & w = ~ (uncurry l) holds
y = O .. (curry w) ) ) ) )
then reconsider Z = dom w as non empty set ;
reconsider p = ~ (uncurry w) as ManySortedSet of [:J,Z:] ;
take y = O .. (curry p); ::_thesis: ( y in product B & ( for l being Element of (product B) * st l = x holds
( ( dom l = {} implies y = O .. (EmptySeq B) ) & ( dom l <> {} implies for Z being non empty set
for w being ManySortedSet of [:J,Z:] st Z = dom l & w = ~ (uncurry l) holds
y = O .. (curry w) ) ) ) )
A8: for z being set st z in dom B holds
(O .. (curry p)) . z in B . z
proof
let z be set ; ::_thesis: ( z in dom B implies (O .. (curry p)) . z in B . z )
assume z in dom B ; ::_thesis: (O .. (curry p)) . z in B . z
then reconsider j = z as Element of J by PARTFUN1:def_2;
A9: dom p = [:J,Z:] by PARTFUN1:def_2;
then proj1 (dom p) = J by FUNCT_5:9;
then consider g being Function such that
A10: (curry p) . j = g and
A11: dom g = proj2 ((dom p) /\ [:{j},(proj2 (dom p)):]) and
A12: for y being set st y in dom g holds
g . y = p . (j,y) by FUNCT_5:def_1;
proj2 (dom p) = Z by A9, FUNCT_5:9;
then A13: dom g = proj2 [:(J /\ {j}),(Z /\ Z):] by A9, A11, ZFMISC_1:100
.= proj2 [:{j},Z:] by ZFMISC_1:46
.= dom w by FUNCT_5:9
.= Seg (len w) by FINSEQ_1:def_3 ;
then reconsider g = g as FinSequence by FINSEQ_1:def_2;
rng g c= B . j
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng g or y in B . j )
assume y in rng g ; ::_thesis: y in B . j
then consider x being set such that
A14: x in dom g and
A15: g . x = y by FUNCT_1:def_3;
( dom (uncurry w) = [:(dom w),J:] & dom g = dom w ) by A13, FINSEQ_1:def_3, PARTFUN1:def_2;
then A16: [x,j] in dom (uncurry w) by A14, ZFMISC_1:87;
then consider a being set , f being Function, b being set such that
A17: [x,j] = [a,b] and
A18: a in dom w and
A19: f = w . a and
A20: b in dom f by FUNCT_5:def_2;
y = (~ (uncurry w)) . (j,x) by A12, A14, A15;
then A21: y = (uncurry w) . (x,j) by A16, FUNCT_4:def_2;
( [a,b] `1 = a & [a,b] `2 = j ) by A17, MCART_1:7;
then A22: y = f . j by A16, A21, A17, A19, FUNCT_5:def_2;
A23: j = b by A17, XTUPLE_0:1;
A24: ( rng w c= product B & w . a in rng w ) by A18, FINSEQ_1:def_4, FUNCT_1:def_3;
then dom f = dom B by A19, CARD_3:9;
hence y in B . j by A19, A20, A23, A24, A22, CARD_3:9; ::_thesis: verum
end;
then reconsider g = g as FinSequence of B . j by FINSEQ_1:def_4;
reconsider g = g as Element of (B . j) * by FINSEQ_1:def_11;
arity (O . j) = ComAr O by Def19;
then A25: dom (O . j) = (ComAr O) -tuples_on (B . j) by MARGREL1:22
.= { s where s is Element of (B . j) * : len s = ComAr O } ;
len g = len w by A13, FINSEQ_1:def_3;
then g in dom (O . j) by A3, A25;
then A26: (O . j) . g in rng (O . j) by FUNCT_1:def_3;
( (O .. (curry p)) . z = (O . j) . ((curry p) . j) & rng (O . j) c= B . j ) by Def18, RELAT_1:def_19;
hence (O .. (curry p)) . z in B . z by A10, A26; ::_thesis: verum
end;
dom (O .. (curry p)) = J by PARTFUN1:def_2
.= dom B by PARTFUN1:def_2 ;
hence y in product B by A8, CARD_3:def_5; ::_thesis: for l being Element of (product B) * st l = x holds
( ( dom l = {} implies y = O .. (EmptySeq B) ) & ( dom l <> {} implies for Z being non empty set
for w being ManySortedSet of [:J,Z:] st Z = dom l & w = ~ (uncurry l) holds
y = O .. (curry w) ) )
let l be Element of (product B) * ; ::_thesis: ( l = x implies ( ( dom l = {} implies y = O .. (EmptySeq B) ) & ( dom l <> {} implies for Z being non empty set
for w being ManySortedSet of [:J,Z:] st Z = dom l & w = ~ (uncurry l) holds
y = O .. (curry w) ) ) )
assume l = x ; ::_thesis: ( ( dom l = {} implies y = O .. (EmptySeq B) ) & ( dom l <> {} implies for Z being non empty set
for w being ManySortedSet of [:J,Z:] st Z = dom l & w = ~ (uncurry l) holds
y = O .. (curry w) ) )
hence ( ( dom l = {} implies y = O .. (EmptySeq B) ) & ( dom l <> {} implies for Z being non empty set
for w being ManySortedSet of [:J,Z:] st Z = dom l & w = ~ (uncurry l) holds
y = O .. (curry w) ) ) by A2; ::_thesis: verum
end;
end;
end;
hence ex y being set st
( y in product B & S1[x,y] ) ; ::_thesis: verum
end;
consider f being Function such that
A27: ( dom f = (ComAr O) -tuples_on (product B) & rng f c= product B & ( for x being set st x in (ComAr O) -tuples_on (product B) holds
S1[x,f . x] ) ) from FUNCT_1:sch_5(A1);
ComAr O in NAT by ORDINAL1:def_12;
then (ComAr O) -tuples_on (product B) in { (n -tuples_on (product B)) where n is Element of NAT : verum } ;
then A28: (ComAr O) -tuples_on (product B) c= union { (m -tuples_on (product B)) where m is Element of NAT : verum } by ZFMISC_1:74;
then dom f c= (product B) * by A27, FINSEQ_2:108;
then reconsider f = f as PartFunc of ((product B) *),(product B) by A27, RELSET_1:4;
A29: f is homogeneous
proof
let x, y be FinSequence; :: according to MARGREL1:def_1,MARGREL1:def_21 ::_thesis: ( not x in proj1 f or not y in proj1 f or len x = len y )
assume A30: ( x in dom f & y in dom f ) ; ::_thesis: len x = len y
then reconsider x1 = x, y1 = y as Element of (product B) * by A27, A28, FINSEQ_2:108;
( ex w being Element of (product B) * st
( x1 = w & len w = ComAr O ) & ex w being Element of (product B) * st
( y1 = w & len w = ComAr O ) ) by A27, A30;
hence len x = len y ; ::_thesis: verum
end;
f is quasi_total
proof
let x, y be FinSequence of product B; :: according to MARGREL1:def_22 ::_thesis: ( not len x = len y or not x in proj1 f or y in proj1 f )
assume that
A31: len x = len y and
A32: x in dom f ; ::_thesis: y in proj1 f
reconsider x1 = x, y1 = y as Element of (product B) * by FINSEQ_1:def_11;
ex w being Element of (product B) * st
( x1 = w & len w = ComAr O ) by A27, A32;
then y1 in { q where q is Element of (product B) * : len q = ComAr O } by A31;
hence y in proj1 f by A27; ::_thesis: verum
end;
then reconsider f = f as non empty homogeneous quasi_total PartFunc of ((product B) *),(product B) by A27, A29;
take f ; ::_thesis: ( dom f = (ComAr O) -tuples_on (product B) & ( for p being Element of (product B) * st p in dom f holds
( ( dom p = {} implies f . p = O .. (EmptySeq B) ) & ( dom p <> {} implies for Z being non empty set
for w being ManySortedSet of [:J,Z:] st Z = dom p & w = ~ (uncurry p) holds
f . p = O .. (curry w) ) ) ) )
thus dom f = (ComAr O) -tuples_on (product B) by A27; ::_thesis: for p being Element of (product B) * st p in dom f holds
( ( dom p = {} implies f . p = O .. (EmptySeq B) ) & ( dom p <> {} implies for Z being non empty set
for w being ManySortedSet of [:J,Z:] st Z = dom p & w = ~ (uncurry p) holds
f . p = O .. (curry w) ) )
let p be Element of (product B) * ; ::_thesis: ( p in dom f implies ( ( dom p = {} implies f . p = O .. (EmptySeq B) ) & ( dom p <> {} implies for Z being non empty set
for w being ManySortedSet of [:J,Z:] st Z = dom p & w = ~ (uncurry p) holds
f . p = O .. (curry w) ) ) )
assume p in dom f ; ::_thesis: ( ( dom p = {} implies f . p = O .. (EmptySeq B) ) & ( dom p <> {} implies for Z being non empty set
for w being ManySortedSet of [:J,Z:] st Z = dom p & w = ~ (uncurry p) holds
f . p = O .. (curry w) ) )
hence ( ( dom p = {} implies f . p = O .. (EmptySeq B) ) & ( dom p <> {} implies for Z being non empty set
for w being ManySortedSet of [:J,Z:] st Z = dom p & w = ~ (uncurry p) holds
f . p = O .. (curry w) ) ) by A27; ::_thesis: verum
end;
uniqueness
for b1, b2 being non empty homogeneous quasi_total PartFunc of ((product B) *),(product B) st dom b1 = (ComAr O) -tuples_on (product B) & ( for p being Element of (product B) * st p in dom b1 holds
( ( dom p = {} implies b1 . p = O .. (EmptySeq B) ) & ( dom p <> {} implies for Z being non empty set
for w being ManySortedSet of [:J,Z:] st Z = dom p & w = ~ (uncurry p) holds
b1 . p = O .. (curry w) ) ) ) & dom b2 = (ComAr O) -tuples_on (product B) & ( for p being Element of (product B) * st p in dom b2 holds
( ( dom p = {} implies b2 . p = O .. (EmptySeq B) ) & ( dom p <> {} implies for Z being non empty set
for w being ManySortedSet of [:J,Z:] st Z = dom p & w = ~ (uncurry p) holds
b2 . p = O .. (curry w) ) ) ) holds
b1 = b2
proof
set pr = product B;
set ca = ComAr O;
let f, g be non empty homogeneous quasi_total PartFunc of ((product B) *),(product B); ::_thesis: ( dom f = (ComAr O) -tuples_on (product B) & ( for p being Element of (product B) * st p in dom f holds
( ( dom p = {} implies f . p = O .. (EmptySeq B) ) & ( dom p <> {} implies for Z being non empty set
for w being ManySortedSet of [:J,Z:] st Z = dom p & w = ~ (uncurry p) holds
f . p = O .. (curry w) ) ) ) & dom g = (ComAr O) -tuples_on (product B) & ( for p being Element of (product B) * st p in dom g holds
( ( dom p = {} implies g . p = O .. (EmptySeq B) ) & ( dom p <> {} implies for Z being non empty set
for w being ManySortedSet of [:J,Z:] st Z = dom p & w = ~ (uncurry p) holds
g . p = O .. (curry w) ) ) ) implies f = g )
assume that
A33: dom f = (ComAr O) -tuples_on (product B) and
A34: for p being Element of (product B) * st p in dom f holds
( ( dom p = {} implies f . p = O .. (EmptySeq B) ) & ( dom p <> {} implies for Z being non empty set
for w being ManySortedSet of [:J,Z:] st Z = dom p & w = ~ (uncurry p) holds
f . p = O .. (curry w) ) ) and
A35: dom g = (ComAr O) -tuples_on (product B) and
A36: for p being Element of (product B) * st p in dom g holds
( ( dom p = {} implies g . p = O .. (EmptySeq B) ) & ( dom p <> {} implies for Z being non empty set
for w being ManySortedSet of [:J,Z:] st Z = dom p & w = ~ (uncurry p) holds
g . p = O .. (curry w) ) ) ; ::_thesis: f = g
for x being set st x in (ComAr O) -tuples_on (product B) holds
f . x = g . x
proof
let x be set ; ::_thesis: ( x in (ComAr O) -tuples_on (product B) implies f . x = g . x )
assume A37: x in (ComAr O) -tuples_on (product B) ; ::_thesis: f . x = g . x
then consider s being Element of (product B) * such that
A38: x = s and
len s = ComAr O ;
now__::_thesis:_(_(_dom_s_=_{}_&_f_._x_=_g_._x_)_or_(_dom_s_<>_{}_&_f_._x_=_g_._x_)_)
percases ( dom s = {} or dom s <> {} ) ;
caseA39: dom s = {} ; ::_thesis: f . x = g . x
then f . s = O .. (EmptySeq B) by A33, A34, A37, A38;
hence f . x = g . x by A35, A36, A37, A38, A39; ::_thesis: verum
end;
case dom s <> {} ; ::_thesis: f . x = g . x
then reconsider Z = dom s as non empty set ;
reconsider w = ~ (uncurry s) as ManySortedSet of [:J,Z:] ;
f . s = O .. (curry w) by A33, A34, A37, A38;
hence f . x = g . x by A35, A36, A37, A38; ::_thesis: verum
end;
end;
end;
hence f . x = g . x ; ::_thesis: verum
end;
hence f = g by A33, A35, FUNCT_1:2; ::_thesis: verum
end;
end;
:: deftheorem defines [[: PRALG_1:def_21_:_
for J being non empty set
for B being V2() ManySortedSet of J
for O being equal-arity ManySortedOperation of B
for b4 being non empty homogeneous quasi_total PartFunc of ((product B) *),(product B) holds
( b4 = [[:O:]] iff ( dom b4 = (ComAr O) -tuples_on (product B) & ( for p being Element of (product B) * st p in dom b4 holds
( ( dom p = {} implies b4 . p = O .. (EmptySeq B) ) & ( dom p <> {} implies for Z being non empty set
for w being ManySortedSet of [:J,Z:] st Z = dom p & w = ~ (uncurry p) holds
b4 . p = O .. (curry w) ) ) ) ) );
definition
let J be non empty set ;
let A be Univ_Alg-yielding equal-signature ManySortedSet of J;
let n be Nat;
assume A1: n in dom (ComSign A) ;
func ProdOp (A,n) -> equal-arity ManySortedOperation of Carrier A means :: PRALG_1:def 22
for j being Element of J
for o being operation of (A . j) st the charact of (A . j) . n = o holds
it . j = o;
existence
ex b1 being equal-arity ManySortedOperation of Carrier A st
for j being Element of J
for o being operation of (A . j) st the charact of (A . j) . n = o holds
b1 . j = o
proof
defpred S1[ set , set ] means for j being Element of J st $1 = j holds
for o being operation of (A . j) st the charact of (A . j) . n = o holds
$2 = o;
A2: for x being set st x in J holds
ex y being set st S1[x,y]
proof
let x be set ; ::_thesis: ( x in J implies ex y being set st S1[x,y] )
assume x in J ; ::_thesis: ex y being set st S1[x,y]
then reconsider x1 = x as Element of J ;
n in dom (signature (A . x1)) by A1, Def14;
then n in Seg (len (signature (A . x1))) by FINSEQ_1:def_3;
then n in Seg (len the charact of (A . x1)) by UNIALG_1:def_4;
then n in dom the charact of (A . x1) by FINSEQ_1:def_3;
then reconsider o = the charact of (A . x1) . n as operation of (A . x1) by FUNCT_1:def_3;
take o ; ::_thesis: S1[x,o]
let j be Element of J; ::_thesis: ( x = j implies for o being operation of (A . j) st the charact of (A . j) . n = o holds
o = o )
assume A3: x = j ; ::_thesis: for o being operation of (A . j) st the charact of (A . j) . n = o holds
o = o
let o1 be operation of (A . j); ::_thesis: ( the charact of (A . j) . n = o1 implies o = o1 )
assume the charact of (A . j) . n = o1 ; ::_thesis: o = o1
hence o = o1 by A3; ::_thesis: verum
end;
consider f being Function such that
A4: ( dom f = J & ( for x being set st x in J holds
S1[x,f . x] ) ) from CLASSES1:sch_1(A2);
reconsider f = f as ManySortedSet of J by A4, 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 x1 = x as Element of J by A4;
n in dom (signature (A . x1)) by A1, Def14;
then n in Seg (len (signature (A . x1))) by FINSEQ_1:def_3;
then n in Seg (len the charact of (A . x1)) by UNIALG_1:def_4;
then n in dom the charact of (A . x1) by FINSEQ_1:def_3;
then reconsider o = the charact of (A . x1) . n as operation of (A . x1) by FUNCT_1:def_3;
f . x = o by A4;
hence f . x is Function ; ::_thesis: verum
end;
then reconsider f = f as ManySortedFunction of J by FUNCOP_1:def_6;
for j being Element of J holds f . j is non empty homogeneous quasi_total PartFunc of (((Carrier A) . j) *),((Carrier A) . j)
proof
let j be Element of J; ::_thesis: f . j is non empty homogeneous quasi_total PartFunc of (((Carrier A) . j) *),((Carrier A) . j)
n in dom (signature (A . j)) by A1, Def14;
then n in Seg (len (signature (A . j))) by FINSEQ_1:def_3;
then n in Seg (len the charact of (A . j)) by UNIALG_1:def_4;
then n in dom the charact of (A . j) by FINSEQ_1:def_3;
then reconsider o = the charact of (A . j) . n as operation of (A . j) by FUNCT_1:def_3;
( ex R being 1-sorted st
( R = A . j & (Carrier A) . j = the carrier of R ) & f . j = o ) by A4, Def13;
hence f . j is non empty homogeneous quasi_total PartFunc of (((Carrier A) . j) *),((Carrier A) . j) ; ::_thesis: verum
end;
then reconsider f = f as ManySortedOperation of Carrier A by Def15;
for i, j being Element of J holds arity (f . i) = arity (f . j)
proof
let i, j be Element of J; ::_thesis: arity (f . i) = arity (f . j)
A5: n in dom (signature (A . j)) by A1, Def14;
then A6: n in Seg (len (signature (A . j))) by FINSEQ_1:def_3;
then n in Seg (len the charact of (A . j)) by UNIALG_1:def_4;
then n in dom the charact of (A . j) by FINSEQ_1:def_3;
then reconsider o = the charact of (A . j) . n as operation of (A . j) by FUNCT_1:def_3;
A7: (signature (A . j)) . n = arity o by A5, UNIALG_1:def_4;
dom A = J by PARTFUN1:def_2;
then A8: signature (A . i) = signature (A . j) by Def12;
then n in Seg (len the charact of (A . i)) by A6, UNIALG_1:def_4;
then n in dom the charact of (A . i) by FINSEQ_1:def_3;
then reconsider o1 = the charact of (A . i) . n as operation of (A . i) by FUNCT_1:def_3;
( arity (f . j) = arity o & f . i = o1 ) by A4;
hence arity (f . i) = arity (f . j) by A8, A5, A7, UNIALG_1:def_4; ::_thesis: verum
end;
then reconsider f = f as equal-arity ManySortedOperation of Carrier A by Th11;
take f ; ::_thesis: for j being Element of J
for o being operation of (A . j) st the charact of (A . j) . n = o holds
f . j = o
let j be Element of J; ::_thesis: for o being operation of (A . j) st the charact of (A . j) . n = o holds
f . j = o
let o be operation of (A . j); ::_thesis: ( the charact of (A . j) . n = o implies f . j = o )
assume the charact of (A . j) . n = o ; ::_thesis: f . j = o
hence f . j = o by A4; ::_thesis: verum
end;
uniqueness
for b1, b2 being equal-arity ManySortedOperation of Carrier A st ( for j being Element of J
for o being operation of (A . j) st the charact of (A . j) . n = o holds
b1 . j = o ) & ( for j being Element of J
for o being operation of (A . j) st the charact of (A . j) . n = o holds
b2 . j = o ) holds
b1 = b2
proof
let O1, O2 be equal-arity ManySortedOperation of Carrier A; ::_thesis: ( ( for j being Element of J
for o being operation of (A . j) st the charact of (A . j) . n = o holds
O1 . j = o ) & ( for j being Element of J
for o being operation of (A . j) st the charact of (A . j) . n = o holds
O2 . j = o ) implies O1 = O2 )
assume that
A9: for j being Element of J
for o being operation of (A . j) st the charact of (A . j) . n = o holds
O1 . j = o and
A10: for j being Element of J
for o being operation of (A . j) st the charact of (A . j) . n = o holds
O2 . j = o ; ::_thesis: O1 = O2
for x being set st x in J holds
O1 . x = O2 . x
proof
let x be set ; ::_thesis: ( x in J implies O1 . x = O2 . x )
assume x in J ; ::_thesis: O1 . x = O2 . x
then reconsider x1 = x as Element of J ;
n in dom (signature (A . x1)) by A1, Def14;
then n in Seg (len (signature (A . x1))) by FINSEQ_1:def_3;
then n in Seg (len the charact of (A . x1)) by UNIALG_1:def_4;
then n in dom the charact of (A . x1) by FINSEQ_1:def_3;
then reconsider o = the charact of (A . x1) . n as operation of (A . x1) by FUNCT_1:def_3;
O1 . x1 = o by A9;
hence O1 . x = O2 . x by A10; ::_thesis: verum
end;
hence O1 = O2 by PBOOLE:3; ::_thesis: verum
end;
end;
:: deftheorem defines ProdOp PRALG_1:def_22_:_
for J being non empty set
for A being Univ_Alg-yielding equal-signature ManySortedSet of J
for n being Nat st n in dom (ComSign A) holds
for b4 being equal-arity ManySortedOperation of Carrier A holds
( b4 = ProdOp (A,n) iff for j being Element of J
for o being operation of (A . j) st the charact of (A . j) . n = o holds
b4 . j = o );
definition
let J be non empty set ;
let A be Univ_Alg-yielding equal-signature ManySortedSet of J;
func ProdOpSeq A -> PFuncFinSequence of (product (Carrier A)) means :Def23: :: PRALG_1:def 23
( len it = len (ComSign A) & ( for n being Nat st n in dom it holds
it . n = [[:(ProdOp (A,n)):]] ) );
existence
ex b1 being PFuncFinSequence of (product (Carrier A)) st
( len b1 = len (ComSign A) & ( for n being Nat st n in dom b1 holds
b1 . n = [[:(ProdOp (A,n)):]] ) )
proof
set f = ComSign A;
defpred S1[ Nat, set ] means $2 = [[:(ProdOp (A,$1)):]];
A1: for k being Nat st k in Seg (len (ComSign A)) holds
ex x being Element of PFuncs (((product (Carrier A)) *),(product (Carrier A))) st S1[k,x]
proof
let k be Nat; ::_thesis: ( k in Seg (len (ComSign A)) implies ex x being Element of PFuncs (((product (Carrier A)) *),(product (Carrier A))) st S1[k,x] )
assume k in Seg (len (ComSign A)) ; ::_thesis: ex x being Element of PFuncs (((product (Carrier A)) *),(product (Carrier A))) st S1[k,x]
reconsider a = [[:(ProdOp (A,k)):]] as Element of PFuncs (((product (Carrier A)) *),(product (Carrier A))) by PARTFUN1:45;
take a ; ::_thesis: S1[k,a]
thus S1[k,a] ; ::_thesis: verum
end;
consider p being FinSequence of PFuncs (((product (Carrier A)) *),(product (Carrier A))) such that
A2: ( dom p = Seg (len (ComSign A)) & ( for k being Nat st k in Seg (len (ComSign A)) holds
S1[k,p . k] ) ) from FINSEQ_1:sch_5(A1);
reconsider p = p as PFuncFinSequence of (product (Carrier A)) ;
take p ; ::_thesis: ( len p = len (ComSign A) & ( for n being Nat st n in dom p holds
p . n = [[:(ProdOp (A,n)):]] ) )
thus len p = len (ComSign A) by A2, FINSEQ_1:def_3; ::_thesis: for n being Nat st n in dom p holds
p . n = [[:(ProdOp (A,n)):]]
let n be Nat; ::_thesis: ( n in dom p implies p . n = [[:(ProdOp (A,n)):]] )
assume n in dom p ; ::_thesis: p . n = [[:(ProdOp (A,n)):]]
hence p . n = [[:(ProdOp (A,n)):]] by A2; ::_thesis: verum
end;
uniqueness
for b1, b2 being PFuncFinSequence of (product (Carrier A)) st len b1 = len (ComSign A) & ( for n being Nat st n in dom b1 holds
b1 . n = [[:(ProdOp (A,n)):]] ) & len b2 = len (ComSign A) & ( for n being Nat st n in dom b2 holds
b2 . n = [[:(ProdOp (A,n)):]] ) holds
b1 = b2
proof
let x, y be PFuncFinSequence of (product (Carrier A)); ::_thesis: ( len x = len (ComSign A) & ( for n being Nat st n in dom x holds
x . n = [[:(ProdOp (A,n)):]] ) & len y = len (ComSign A) & ( for n being Nat st n in dom y holds
y . n = [[:(ProdOp (A,n)):]] ) implies x = y )
assume that
A3: len x = len (ComSign A) and
A4: for n being Nat st n in dom x holds
x . n = [[:(ProdOp (A,n)):]] and
A5: len y = len (ComSign A) and
A6: for n being Nat st n in dom y holds
y . n = [[:(ProdOp (A,n)):]] ; ::_thesis: x = y
A7: dom x = Seg (len (ComSign A)) by A3, FINSEQ_1:def_3;
now__::_thesis:_for_n_being_Nat_st_n_in_dom_x_holds_
x_._n_=_y_._n
let n be Nat; ::_thesis: ( n in dom x implies x . n = y . n )
assume n in dom x ; ::_thesis: x . n = y . n
then ( n in dom y & x . n = [[:(ProdOp (A,n)):]] ) by A4, A5, A7, FINSEQ_1:def_3;
hence x . n = y . n by A6; ::_thesis: verum
end;
hence x = y by A3, A5, FINSEQ_2:9; ::_thesis: verum
end;
end;
:: deftheorem Def23 defines ProdOpSeq PRALG_1:def_23_:_
for J being non empty set
for A being Univ_Alg-yielding equal-signature ManySortedSet of J
for b3 being PFuncFinSequence of (product (Carrier A)) holds
( b3 = ProdOpSeq A iff ( len b3 = len (ComSign A) & ( for n being Nat st n in dom b3 holds
b3 . n = [[:(ProdOp (A,n)):]] ) ) );
definition
let J be non empty set ;
let A be Univ_Alg-yielding equal-signature ManySortedSet of J;
func ProdUnivAlg A -> strict Universal_Algebra equals :: PRALG_1:def 24
UAStr(# (product (Carrier A)),(ProdOpSeq A) #);
coherence
UAStr(# (product (Carrier A)),(ProdOpSeq A) #) is strict Universal_Algebra
proof
set j = the Element of J;
set ua = UAStr(# (product (Carrier A)),(ProdOpSeq A) #);
set pr = product (Carrier A);
for n being Nat
for h being PartFunc of ((product (Carrier A)) *),(product (Carrier A)) st n in dom the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) & h = the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) . n holds
h is quasi_total
proof
let n be Nat; ::_thesis: for h being PartFunc of ((product (Carrier A)) *),(product (Carrier A)) st n in dom the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) & h = the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) . n holds
h is quasi_total
let h be PartFunc of ((product (Carrier A)) *),(product (Carrier A)); ::_thesis: ( n in dom the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) & h = the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) . n implies h is quasi_total )
assume that
A1: n in dom the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) and
A2: the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) . n = h ; ::_thesis: h is quasi_total
the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) . n = [[:(ProdOp (A,n)):]] by A1, Def23;
hence h is quasi_total by A2; ::_thesis: verum
end;
then A3: the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) is quasi_total by MARGREL1:def_24;
for n being Nat
for h being PartFunc of ((product (Carrier A)) *),(product (Carrier A)) st n in dom the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) & h = the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) . n holds
h is homogeneous
proof
let n be Nat; ::_thesis: for h being PartFunc of ((product (Carrier A)) *),(product (Carrier A)) st n in dom the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) & h = the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) . n holds
h is homogeneous
let h be PartFunc of ((product (Carrier A)) *),(product (Carrier A)); ::_thesis: ( n in dom the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) & h = the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) . n implies h is homogeneous )
assume that
A4: n in dom the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) and
A5: the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) . n = h ; ::_thesis: h is homogeneous
the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) . n = [[:(ProdOp (A,n)):]] by A4, Def23;
hence h is homogeneous by A5; ::_thesis: verum
end;
then A6: the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) is homogeneous by MARGREL1:def_23;
for n being set st n in dom the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) holds
not the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) . n is empty
proof
let n be set ; ::_thesis: ( n in dom the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) implies not the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) . n is empty )
assume A7: n in dom the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) ; ::_thesis: not the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) . n is empty
then reconsider n9 = n as Element of NAT ;
the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) . n = [[:(ProdOp (A,n9)):]] by A7, Def23;
hence not the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) . n is empty ; ::_thesis: verum
end;
then A8: the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) is non-empty by FUNCT_1:def_9;
len the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) = len (ComSign A) by Def23
.= len (signature (A . the Element of J)) by Def14
.= len the charact of (A . the Element of J) by UNIALG_1:def_4 ;
then the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) <> {} ;
hence UAStr(# (product (Carrier A)),(ProdOpSeq A) #) is strict Universal_Algebra by A3, A6, A8, UNIALG_1:def_1, UNIALG_1:def_2, UNIALG_1:def_3; ::_thesis: verum
end;
end;
:: deftheorem defines ProdUnivAlg PRALG_1:def_24_:_
for J being non empty set
for A being Univ_Alg-yielding equal-signature ManySortedSet of J holds ProdUnivAlg A = UAStr(# (product (Carrier A)),(ProdOpSeq A) #);