:: PRALG_3 semantic presentation
begin
registration
let I be set ;
let S be non empty non void ManySortedSign ;
let AF be MSAlgebra-Family of I,S;
cluster product AF -> non-empty ;
coherence
product AF is non-empty by MSUALG_1:def_3;
end;
registration
let X be with_non-empty_elements set ;
cluster id X -> non-empty ;
coherence
id X is non-empty
proof
reconsider NE = id X as ManySortedSet of X ;
NE is V8()
proof
let i be set ; :: according to PBOOLE:def_13 ::_thesis: ( not i in X or not NE . i is empty )
assume i in X ; ::_thesis: not NE . i is empty
hence not NE . i is empty by FUNCT_1:17; ::_thesis: verum
end;
hence id X is non-empty ; ::_thesis: verum
end;
end;
theorem Th1: :: PRALG_3:1
for f, F being Function
for A being set st f in product F holds
f | A in product (F | A)
proof
let f, F be Function; ::_thesis: for A being set st f in product F holds
f | A in product (F | A)
let A be set ; ::_thesis: ( f in product F implies f | A in product (F | A) )
assume A1: f in product F ; ::_thesis: f | A in product (F | A)
then dom f = dom F by CARD_3:9;
then A2: dom (f | A) = (dom F) /\ A by RELAT_1:61
.= dom (F | A) by RELAT_1:61 ;
for x being set st x in dom (F | A) holds
(f | A) . x in (F | A) . x
proof
let x be set ; ::_thesis: ( x in dom (F | A) implies (f | A) . x in (F | A) . x )
assume A3: x in dom (F | A) ; ::_thesis: (f | A) . x in (F | A) . x
then x in (dom F) /\ A by RELAT_1:61;
then A4: x in dom F by XBOOLE_0:def_4;
( (F | A) . x = F . x & (f | A) . x = f . x ) by A2, A3, FUNCT_1:47;
hence (f | A) . x in (F | A) . x by A1, A4, CARD_3:9; ::_thesis: verum
end;
hence f | A in product (F | A) by A2, CARD_3:9; ::_thesis: verum
end;
theorem Th2: :: PRALG_3:2
for I being non empty set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for s being SortSymbol of S
for a being non empty Subset of I
for Aa being MSAlgebra-Family of a,S st A | a = Aa holds
Carrier (Aa,s) = (Carrier (A,s)) | a
proof
let I be non empty set ; ::_thesis: for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for s being SortSymbol of S
for a being non empty Subset of I
for Aa being MSAlgebra-Family of a,S st A | a = Aa holds
Carrier (Aa,s) = (Carrier (A,s)) | a
let S be non empty non void ManySortedSign ; ::_thesis: for A being MSAlgebra-Family of I,S
for s being SortSymbol of S
for a being non empty Subset of I
for Aa being MSAlgebra-Family of a,S st A | a = Aa holds
Carrier (Aa,s) = (Carrier (A,s)) | a
let A be MSAlgebra-Family of I,S; ::_thesis: for s being SortSymbol of S
for a being non empty Subset of I
for Aa being MSAlgebra-Family of a,S st A | a = Aa holds
Carrier (Aa,s) = (Carrier (A,s)) | a
let s be SortSymbol of S; ::_thesis: for a being non empty Subset of I
for Aa being MSAlgebra-Family of a,S st A | a = Aa holds
Carrier (Aa,s) = (Carrier (A,s)) | a
let a be non empty Subset of I; ::_thesis: for Aa being MSAlgebra-Family of a,S st A | a = Aa holds
Carrier (Aa,s) = (Carrier (A,s)) | a
let Aa be MSAlgebra-Family of a,S; ::_thesis: ( A | a = Aa implies Carrier (Aa,s) = (Carrier (A,s)) | a )
assume A1: A | a = Aa ; ::_thesis: Carrier (Aa,s) = (Carrier (A,s)) | a
dom ((Carrier (A,s)) | a) = (dom (Carrier (A,s))) /\ a by RELAT_1:61
.= I /\ a by PARTFUN1:def_2
.= a by XBOOLE_1:28 ;
then reconsider Cas = (Carrier (A,s)) | a as ManySortedSet of a by PARTFUN1:def_2;
for i being set st i in a holds
(Carrier (Aa,s)) . i = Cas . i
proof
let i be set ; ::_thesis: ( i in a implies (Carrier (Aa,s)) . i = Cas . i )
assume A2: i in a ; ::_thesis: (Carrier (Aa,s)) . i = Cas . i
then reconsider i9 = i as Element of a ;
reconsider i99 = i9 as Element of I ;
A3: ( Aa . i9 = A . i9 & ex U1 being MSAlgebra over S st
( U1 = A . i99 & (Carrier (A,s)) . i99 = the Sorts of U1 . s ) ) by A1, FUNCT_1:49, PRALG_2:def_9;
ex U0 being MSAlgebra over S st
( U0 = Aa . i & (Carrier (Aa,s)) . i = the Sorts of U0 . s ) by A2, PRALG_2:def_9;
hence (Carrier (Aa,s)) . i = Cas . i by A3, FUNCT_1:49; ::_thesis: verum
end;
hence Carrier (Aa,s) = (Carrier (A,s)) | a by PBOOLE:3; ::_thesis: verum
end;
theorem Th3: :: PRALG_3:3
for i being set
for I being non empty set
for EqR being Equivalence_Relation of I
for c1, c2 being Element of Class EqR st i in c1 & i in c2 holds
c1 = c2
proof
let i be set ; ::_thesis: for I being non empty set
for EqR being Equivalence_Relation of I
for c1, c2 being Element of Class EqR st i in c1 & i in c2 holds
c1 = c2
let I be non empty set ; ::_thesis: for EqR being Equivalence_Relation of I
for c1, c2 being Element of Class EqR st i in c1 & i in c2 holds
c1 = c2
let EqR be Equivalence_Relation of I; ::_thesis: for c1, c2 being Element of Class EqR st i in c1 & i in c2 holds
c1 = c2
let c1, c2 be Element of Class EqR; ::_thesis: ( i in c1 & i in c2 implies c1 = c2 )
assume that
A1: i in c1 and
A2: i in c2 ; ::_thesis: c1 = c2
consider x1 being set such that
x1 in I and
A3: c1 = Class (EqR,x1) by EQREL_1:def_3;
A4: [i,x1] in EqR by A1, A3, EQREL_1:19;
consider x2 being set such that
x2 in I and
A5: c2 = Class (EqR,x2) by EQREL_1:def_3;
[i,x2] in EqR by A2, A5, EQREL_1:19;
then Class (EqR,x2) = Class (EqR,i) by A1, EQREL_1:35
.= c1 by A1, A3, A4, EQREL_1:35 ;
hence c1 = c2 by A5; ::_thesis: verum
end;
Lm1: for f being Function
for x being set st x in product f holds
x is Function
;
theorem :: PRALG_3:4
for D being non empty set
for F being ManySortedFunction of D
for C being non empty functional with_common_domain set st C = rng F holds
for d being Element of D
for e being set st e in DOM C holds
(F . d) . e = ((commute F) . e) . d
proof
let D be non empty set ; ::_thesis: for F being ManySortedFunction of D
for C being non empty functional with_common_domain set st C = rng F holds
for d being Element of D
for e being set st e in DOM C holds
(F . d) . e = ((commute F) . e) . d
let F be ManySortedFunction of D; ::_thesis: for C being non empty functional with_common_domain set st C = rng F holds
for d being Element of D
for e being set st e in DOM C holds
(F . d) . e = ((commute F) . e) . d
set E = union { (rng (F . d9)) where d9 is Element of D : verum } ;
reconsider F9 = F as Function ;
let C be non empty functional with_common_domain set ; ::_thesis: ( C = rng F implies for d being Element of D
for e being set st e in DOM C holds
(F . d) . e = ((commute F) . e) . d )
assume A1: C = rng F ; ::_thesis: for d being Element of D
for e being set st e in DOM C holds
(F . d) . e = ((commute F) . e) . d
A2: rng F9 c= Funcs ((DOM C),(union { (rng (F . d9)) where d9 is Element of D : verum } ))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng F9 or x in Funcs ((DOM C),(union { (rng (F . d9)) where d9 is Element of D : verum } )) )
assume x in rng F9 ; ::_thesis: x in Funcs ((DOM C),(union { (rng (F . d9)) where d9 is Element of D : verum } ))
then consider d9 being set such that
A3: d9 in dom F and
A4: F . d9 = x by FUNCT_1:def_3;
reconsider d9 = d9 as Element of D by A3;
consider Fd being Function such that
A5: Fd = F . d9 ;
A6: rng Fd c= union { (rng (F . d9)) where d9 is Element of D : verum }
proof
A7: rng Fd in { (rng (F . d99)) where d99 is Element of D : verum } by A5;
let x1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not x1 in rng Fd or x1 in union { (rng (F . d9)) where d9 is Element of D : verum } )
assume x1 in rng Fd ; ::_thesis: x1 in union { (rng (F . d9)) where d9 is Element of D : verum }
hence x1 in union { (rng (F . d9)) where d9 is Element of D : verum } by A7, TARSKI:def_4; ::_thesis: verum
end;
F . d9 in rng F by A3, FUNCT_1:def_3;
then dom Fd = DOM C by A1, A5, CARD_3:108;
hence x in Funcs ((DOM C),(union { (rng (F . d9)) where d9 is Element of D : verum } )) by A4, A5, A6, FUNCT_2:def_2; ::_thesis: verum
end;
let d be Element of D; ::_thesis: for e being set st e in DOM C holds
(F . d) . e = ((commute F) . e) . d
let e be set ; ::_thesis: ( e in DOM C implies (F . d) . e = ((commute F) . e) . d )
assume A8: e in DOM C ; ::_thesis: (F . d) . e = ((commute F) . e) . d
dom F9 = D by PARTFUN1:def_2;
then F in Funcs (D,(Funcs ((DOM C),(union { (rng (F . d9)) where d9 is Element of D : verum } )))) by A2, FUNCT_2:def_2;
hence (F . d) . e = ((commute F) . e) . d by A8, FUNCT_6:56; ::_thesis: verum
end;
begin
definition
let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra over S;
let o be OperSymbol of S;
func const (o,U0) -> set equals :: PRALG_3:def 1
(Den (o,U0)) . {};
correctness
coherence
(Den (o,U0)) . {} is set ;
;
end;
:: deftheorem defines const PRALG_3:def_1_:_
for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for o being OperSymbol of S holds const (o,U0) = (Den (o,U0)) . {};
theorem Th5: :: PRALG_3:5
for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for o being OperSymbol of S st the_arity_of o = {} & Result (o,U0) <> {} holds
const (o,U0) in Result (o,U0)
proof
let S be non empty non void ManySortedSign ; ::_thesis: for U0 being MSAlgebra over S
for o being OperSymbol of S st the_arity_of o = {} & Result (o,U0) <> {} holds
const (o,U0) in Result (o,U0)
let U0 be MSAlgebra over S; ::_thesis: for o being OperSymbol of S st the_arity_of o = {} & Result (o,U0) <> {} holds
const (o,U0) in Result (o,U0)
let o be OperSymbol of S; ::_thesis: ( the_arity_of o = {} & Result (o,U0) <> {} implies const (o,U0) in Result (o,U0) )
assume that
A1: the_arity_of o = {} and
A2: Result (o,U0) <> {} ; ::_thesis: const (o,U0) in Result (o,U0)
dom (Den (o,U0)) = Args (o,U0) by A2, FUNCT_2:def_1
.= {{}} by A1, PRALG_2:4 ;
then {} in dom (Den (o,U0)) by TARSKI:def_1;
then (Den (o,U0)) . {} in rng (Den (o,U0)) by FUNCT_1:def_3;
hence const (o,U0) in Result (o,U0) ; ::_thesis: verum
end;
theorem :: PRALG_3:6
for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for s being SortSymbol of S st the Sorts of U0 . s <> {} holds
Constants (U0,s) = { (const (o,U0)) where o is Element of the carrier' of S : ( the_result_sort_of o = s & the_arity_of o = {} ) }
proof
let S be non empty non void ManySortedSign ; ::_thesis: for U0 being MSAlgebra over S
for s being SortSymbol of S st the Sorts of U0 . s <> {} holds
Constants (U0,s) = { (const (o,U0)) where o is Element of the carrier' of S : ( the_result_sort_of o = s & the_arity_of o = {} ) }
let U0 be MSAlgebra over S; ::_thesis: for s being SortSymbol of S st the Sorts of U0 . s <> {} holds
Constants (U0,s) = { (const (o,U0)) where o is Element of the carrier' of S : ( the_result_sort_of o = s & the_arity_of o = {} ) }
let s be SortSymbol of S; ::_thesis: ( the Sorts of U0 . s <> {} implies Constants (U0,s) = { (const (o,U0)) where o is Element of the carrier' of S : ( the_result_sort_of o = s & the_arity_of o = {} ) } )
assume A1: the Sorts of U0 . s <> {} ; ::_thesis: Constants (U0,s) = { (const (o,U0)) where o is Element of the carrier' of S : ( the_result_sort_of o = s & the_arity_of o = {} ) }
thus Constants (U0,s) c= { (const (o,U0)) where o is Element of the carrier' of S : ( the_result_sort_of o = s & the_arity_of o = {} ) } :: according to XBOOLE_0:def_10 ::_thesis: { (const (o,U0)) where o is Element of the carrier' of S : ( the_result_sort_of o = s & the_arity_of o = {} ) } c= Constants (U0,s)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Constants (U0,s) or x in { (const (o,U0)) where o is Element of the carrier' of S : ( the_result_sort_of o = s & the_arity_of o = {} ) } )
assume A2: x in Constants (U0,s) ; ::_thesis: x in { (const (o,U0)) where o is Element of the carrier' of S : ( the_result_sort_of o = s & the_arity_of o = {} ) }
ex A being non empty set st
( A = the Sorts of U0 . s & Constants (U0,s) = { a where a is Element of A : ex o being OperSymbol of S st
( the Arity of S . o = {} & the ResultSort of S . o = s & a in rng (Den (o,U0)) ) } ) by A1, MSUALG_2:def_3;
then consider A being non empty set such that
A = the Sorts of U0 . s and
A3: x in { a where a is Element of A : ex o being OperSymbol of S st
( the Arity of S . o = {} & the ResultSort of S . o = s & a in rng (Den (o,U0)) ) } by A2;
consider a being Element of A such that
A4: a = x and
A5: ex o being OperSymbol of S st
( the Arity of S . o = {} & the ResultSort of S . o = s & a in rng (Den (o,U0)) ) by A3;
consider o1 being OperSymbol of S such that
A6: the Arity of S . o1 = {} and
A7: the ResultSort of S . o1 = s and
A8: a in rng (Den (o1,U0)) by A5;
A9: ex x1 being set st
( x1 in dom (Den (o1,U0)) & a = (Den (o1,U0)) . x1 ) by A8, FUNCT_1:def_3;
A10: the_result_sort_of o1 = s by A7, MSUALG_1:def_2;
A11: the_arity_of o1 = {} by A6, MSUALG_1:def_1;
then Args (o1,U0) = {{}} by PRALG_2:4;
then x = const (o1,U0) by A4, A9, TARSKI:def_1;
hence x in { (const (o,U0)) where o is Element of the carrier' of S : ( the_result_sort_of o = s & the_arity_of o = {} ) } by A10, A11; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (const (o,U0)) where o is Element of the carrier' of S : ( the_result_sort_of o = s & the_arity_of o = {} ) } or x in Constants (U0,s) )
assume x in { (const (o,U0)) where o is Element of the carrier' of S : ( the_result_sort_of o = s & the_arity_of o = {} ) } ; ::_thesis: x in Constants (U0,s)
then consider o being Element of the carrier' of S such that
A12: x = const (o,U0) and
A13: the_result_sort_of o = s and
A14: the_arity_of o = {} ;
o in the carrier' of S ;
then A15: o in dom the ResultSort of S by FUNCT_2:def_1;
A16: Result (o,U0) = ( the Sorts of U0 * the ResultSort of S) . o by MSUALG_1:def_5
.= the Sorts of U0 . ( the ResultSort of S . o) by A15, FUNCT_1:13
.= the Sorts of U0 . s by A13, MSUALG_1:def_2 ;
thus x in Constants (U0,s) ::_thesis: verum
proof
A17: ex o being OperSymbol of S st
( the Arity of S . o = {} & the ResultSort of S . o = s & x in rng (Den (o,U0)) )
proof
take o ; ::_thesis: ( the Arity of S . o = {} & the ResultSort of S . o = s & x in rng (Den (o,U0)) )
( Args (o,U0) = dom (Den (o,U0)) & Args (o,U0) = {{}} ) by A1, A14, A16, FUNCT_2:def_1, PRALG_2:4;
then {} in dom (Den (o,U0)) by TARSKI:def_1;
hence ( the Arity of S . o = {} & the ResultSort of S . o = s & x in rng (Den (o,U0)) ) by A12, A13, A14, FUNCT_1:def_3, MSUALG_1:def_1, MSUALG_1:def_2; ::_thesis: verum
end;
consider A being non empty set such that
A18: A = the Sorts of U0 . s and
A19: Constants (U0,s) = { a where a is Element of A : ex o being OperSymbol of S st
( the Arity of S . o = {} & the ResultSort of S . o = s & a in rng (Den (o,U0)) ) } by A1, MSUALG_2:def_3;
x is Element of A by A12, A14, A16, A18, Th5;
hence x in Constants (U0,s) by A19, A17; ::_thesis: verum
end;
end;
theorem Th7: :: PRALG_3:7
for I being non empty set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S st the_arity_of o = {} holds
(commute (OPER A)) . o in Funcs (I,(Funcs ({{}},(union { (Result (o,(A . i9))) where i9 is Element of I : verum } ))))
proof
let I be non empty set ; ::_thesis: for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S st the_arity_of o = {} holds
(commute (OPER A)) . o in Funcs (I,(Funcs ({{}},(union { (Result (o,(A . i9))) where i9 is Element of I : verum } ))))
let S be non empty non void ManySortedSign ; ::_thesis: for A being MSAlgebra-Family of I,S
for o being OperSymbol of S st the_arity_of o = {} holds
(commute (OPER A)) . o in Funcs (I,(Funcs ({{}},(union { (Result (o,(A . i9))) where i9 is Element of I : verum } ))))
let A be MSAlgebra-Family of I,S; ::_thesis: for o being OperSymbol of S st the_arity_of o = {} holds
(commute (OPER A)) . o in Funcs (I,(Funcs ({{}},(union { (Result (o,(A . i9))) where i9 is Element of I : verum } ))))
let o be OperSymbol of S; ::_thesis: ( the_arity_of o = {} implies (commute (OPER A)) . o in Funcs (I,(Funcs ({{}},(union { (Result (o,(A . i9))) where i9 is Element of I : verum } )))) )
set f = (commute (OPER A)) . o;
set C = union { (Result (o,(A . i9))) where i9 is Element of I : verum } ;
commute (OPER A) in Funcs ( the carrier' of S,(Funcs (I,(rng (uncurry (OPER A)))))) by PRALG_2:6;
then A1: ex f1 being Function st
( commute (OPER A) = f1 & dom f1 = the carrier' of S & rng f1 c= Funcs (I,(rng (uncurry (OPER A)))) ) by FUNCT_2:def_2;
then (commute (OPER A)) . o in rng (commute (OPER A)) by FUNCT_1:def_3;
then A2: ex fb being Function st
( fb = (commute (OPER A)) . o & dom fb = I & rng fb c= rng (uncurry (OPER A)) ) by A1, FUNCT_2:def_2;
assume A3: the_arity_of o = {} ; ::_thesis: (commute (OPER A)) . o in Funcs (I,(Funcs ({{}},(union { (Result (o,(A . i9))) where i9 is Element of I : verum } ))))
now__::_thesis:_for_x_being_set_st_x_in_rng_((commute_(OPER_A))_._o)_holds_
x_in_Funcs_({{}},(union__{__(Result_(o,(A_._i9)))_where_i9_is_Element_of_I_:_verum__}__))
let x be set ; ::_thesis: ( x in rng ((commute (OPER A)) . o) implies x in Funcs ({{}},(union { (Result (o,(A . i9))) where i9 is Element of I : verum } )) )
assume x in rng ((commute (OPER A)) . o) ; ::_thesis: x in Funcs ({{}},(union { (Result (o,(A . i9))) where i9 is Element of I : verum } ))
then consider a being set such that
A4: a in dom ((commute (OPER A)) . o) and
A5: ((commute (OPER A)) . o) . a = x by FUNCT_1:def_3;
(commute (OPER A)) . o = A ?. o ;
then reconsider x9 = x as Function by A5;
reconsider a = a as Element of I by A2, A4;
A6: x9 = (A ?. o) . a by A5
.= Den (o,(A . a)) by PRALG_2:7 ;
then A7: dom x9 = Args (o,(A . a)) by FUNCT_2:def_1
.= {{}} by A3, PRALG_2:4 ;
now__::_thesis:_for_c_being_set_st_c_in_rng_x9_holds_
c_in_union__{__(Result_(o,(A_._i9)))_where_i9_is_Element_of_I_:_verum__}_
let c be set ; ::_thesis: ( c in rng x9 implies c in union { (Result (o,(A . i9))) where i9 is Element of I : verum } )
assume c in rng x9 ; ::_thesis: c in union { (Result (o,(A . i9))) where i9 is Element of I : verum }
then consider b being set such that
A8: b in dom x9 and
A9: x9 . b = c by FUNCT_1:def_3;
x9 . b = const (o,(A . a)) by A6, A7, A8, TARSKI:def_1;
then A10: c is Element of Result (o,(A . a)) by A3, A9, Th5;
Result (o,(A . a)) in { (Result (o,(A . i9))) where i9 is Element of I : verum } ;
hence c in union { (Result (o,(A . i9))) where i9 is Element of I : verum } by A10, TARSKI:def_4; ::_thesis: verum
end;
then rng x9 c= union { (Result (o,(A . i9))) where i9 is Element of I : verum } by TARSKI:def_3;
hence x in Funcs ({{}},(union { (Result (o,(A . i9))) where i9 is Element of I : verum } )) by A7, FUNCT_2:def_2; ::_thesis: verum
end;
then rng ((commute (OPER A)) . o) c= Funcs ({{}},(union { (Result (o,(A . i9))) where i9 is Element of I : verum } )) by TARSKI:def_3;
hence (commute (OPER A)) . o in Funcs (I,(Funcs ({{}},(union { (Result (o,(A . i9))) where i9 is Element of I : verum } )))) by A2, FUNCT_2:def_2; ::_thesis: verum
end;
theorem Th8: :: PRALG_3:8
for I being non empty set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S st the_arity_of o = {} holds
const (o,(product A)) in Funcs (I,(union { (Result (o,(A . i9))) where i9 is Element of I : verum } ))
proof
let I be non empty set ; ::_thesis: for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S st the_arity_of o = {} holds
const (o,(product A)) in Funcs (I,(union { (Result (o,(A . i9))) where i9 is Element of I : verum } ))
let S be non empty non void ManySortedSign ; ::_thesis: for A being MSAlgebra-Family of I,S
for o being OperSymbol of S st the_arity_of o = {} holds
const (o,(product A)) in Funcs (I,(union { (Result (o,(A . i9))) where i9 is Element of I : verum } ))
let A be MSAlgebra-Family of I,S; ::_thesis: for o being OperSymbol of S st the_arity_of o = {} holds
const (o,(product A)) in Funcs (I,(union { (Result (o,(A . i9))) where i9 is Element of I : verum } ))
let o be OperSymbol of S; ::_thesis: ( the_arity_of o = {} implies const (o,(product A)) in Funcs (I,(union { (Result (o,(A . i9))) where i9 is Element of I : verum } )) )
set g = (commute (OPER A)) . o;
set C = union { (Result (o,(A . i9))) where i9 is Element of I : verum } ;
assume A1: the_arity_of o = {} ; ::_thesis: const (o,(product A)) in Funcs (I,(union { (Result (o,(A . i9))) where i9 is Element of I : verum } ))
then A2: (commute (OPER A)) . o in Funcs (I,(Funcs ({{}},(union { (Result (o,(A . i9))) where i9 is Element of I : verum } )))) by Th7;
reconsider g = (commute (OPER A)) . o as Function ;
(OPS A) . o = IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o)))) by PRALG_2:def_13
.= commute (A ?. o) by A1, FUNCOP_1:def_8 ;
then A3: const (o,(product A)) = (commute g) . {} by MSUALG_1:def_6;
commute g in Funcs ({{}},(Funcs (I,(union { (Result (o,(A . i9))) where i9 is Element of I : verum } )))) by A2, FUNCT_6:55;
then consider g1 being Function such that
A4: g1 = commute g and
A5: dom g1 = {{}} and
A6: rng g1 c= Funcs (I,(union { (Result (o,(A . i9))) where i9 is Element of I : verum } )) by FUNCT_2:def_2;
{} in {{}} by TARSKI:def_1;
then g1 . {} in rng g1 by A5, FUNCT_1:def_3;
hence const (o,(product A)) in Funcs (I,(union { (Result (o,(A . i9))) where i9 is Element of I : verum } )) by A3, A4, A6; ::_thesis: verum
end;
registration
let S be non empty non void ManySortedSign ;
let I be non empty set ;
let o be OperSymbol of S;
let A be MSAlgebra-Family of I,S;
cluster const (o,(product A)) -> Relation-like Function-like ;
coherence
( const (o,(product A)) is Relation-like & const (o,(product A)) is Function-like )
proof
const (o,(product A)) is Function
proof
percases ( the_arity_of o = {} or the_arity_of o <> {} ) ;
suppose the_arity_of o = {} ; ::_thesis: const (o,(product A)) is Function
then const (o,(product A)) in Funcs (I,(union { (Result (o,(A . i9))) where i9 is Element of I : verum } )) by Th8;
then ex g being Function st
( g = const (o,(product A)) & dom g = I & rng g c= union { (Result (o,(A . i9))) where i9 is Element of I : verum } ) by FUNCT_2:def_2;
hence const (o,(product A)) is Function ; ::_thesis: verum
end;
supposeA1: the_arity_of o <> {} ; ::_thesis: const (o,(product A)) is Function
dom ( the Sorts of (product A) * (the_arity_of o)) = dom (the_arity_of o) by PRALG_2:3;
then A2: dom ( the Sorts of (product A) * (the_arity_of o)) <> dom {} by A1;
dom (Den (o,(product A))) = Args (o,(product A)) by FUNCT_2:def_1
.= product ( the Sorts of (product A) * (the_arity_of o)) by PRALG_2:3 ;
then not {} in dom (Den (o,(product A))) by A2, CARD_3:9;
hence const (o,(product A)) is Function by FUNCT_1:def_2; ::_thesis: verum
end;
end;
end;
hence ( const (o,(product A)) is Relation-like & const (o,(product A)) is Function-like ) ; ::_thesis: verum
end;
end;
theorem Th9: :: PRALG_3:9
for I being non empty set
for S being non empty non void ManySortedSign
for i being Element of I
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S st the_arity_of o = {} holds
(const (o,(product A))) . i = const (o,(A . i))
proof
let I be non empty set ; ::_thesis: for S being non empty non void ManySortedSign
for i being Element of I
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S st the_arity_of o = {} holds
(const (o,(product A))) . i = const (o,(A . i))
let S be non empty non void ManySortedSign ; ::_thesis: for i being Element of I
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S st the_arity_of o = {} holds
(const (o,(product A))) . i = const (o,(A . i))
let i be Element of I; ::_thesis: for A being MSAlgebra-Family of I,S
for o being OperSymbol of S st the_arity_of o = {} holds
(const (o,(product A))) . i = const (o,(A . i))
let A be MSAlgebra-Family of I,S; ::_thesis: for o being OperSymbol of S st the_arity_of o = {} holds
(const (o,(product A))) . i = const (o,(A . i))
let o be OperSymbol of S; ::_thesis: ( the_arity_of o = {} implies (const (o,(product A))) . i = const (o,(A . i)) )
assume A1: the_arity_of o = {} ; ::_thesis: (const (o,(product A))) . i = const (o,(A . i))
set f = (commute (OPER A)) . o;
set C = union { (Result (o,(A . i9))) where i9 is Element of I : verum } ;
A2: (commute (OPER A)) . o in Funcs (I,(Funcs ({{}},(union { (Result (o,(A . i9))) where i9 is Element of I : verum } )))) by A1, Th7;
(OPS A) . o = IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o)))) by PRALG_2:def_13
.= commute (A ?. o) by A1, FUNCOP_1:def_8 ;
then A3: const (o,(product A)) = (commute ((commute (OPER A)) . o)) . {} by MSUALG_1:def_6;
A4: {} in {{}} by TARSKI:def_1;
const (o,(A . i)) = ((A ?. o) . i) . {} by PRALG_2:7
.= (const (o,(product A))) . i by A2, A3, A4, FUNCT_6:56 ;
hence (const (o,(product A))) . i = const (o,(A . i)) ; ::_thesis: verum
end;
theorem :: PRALG_3:10
for I being non empty set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S
for f being Function st the_arity_of o = {} & dom f = I & ( for i being Element of I holds f . i = const (o,(A . i)) ) holds
f = const (o,(product A))
proof
let I be non empty set ; ::_thesis: for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S
for f being Function st the_arity_of o = {} & dom f = I & ( for i being Element of I holds f . i = const (o,(A . i)) ) holds
f = const (o,(product A))
let S be non empty non void ManySortedSign ; ::_thesis: for A being MSAlgebra-Family of I,S
for o being OperSymbol of S
for f being Function st the_arity_of o = {} & dom f = I & ( for i being Element of I holds f . i = const (o,(A . i)) ) holds
f = const (o,(product A))
let A be MSAlgebra-Family of I,S; ::_thesis: for o being OperSymbol of S
for f being Function st the_arity_of o = {} & dom f = I & ( for i being Element of I holds f . i = const (o,(A . i)) ) holds
f = const (o,(product A))
let o be OperSymbol of S; ::_thesis: for f being Function st the_arity_of o = {} & dom f = I & ( for i being Element of I holds f . i = const (o,(A . i)) ) holds
f = const (o,(product A))
let f be Function; ::_thesis: ( the_arity_of o = {} & dom f = I & ( for i being Element of I holds f . i = const (o,(A . i)) ) implies f = const (o,(product A)) )
assume that
A1: the_arity_of o = {} and
A2: dom f = I and
A3: for i being Element of I holds f . i = const (o,(A . i)) ; ::_thesis: f = const (o,(product A))
A4: now__::_thesis:_for_a_being_set_st_a_in_I_holds_
f_._a_=_(const_(o,(product_A)))_._a
let a be set ; ::_thesis: ( a in I implies f . a = (const (o,(product A))) . a )
assume a in I ; ::_thesis: f . a = (const (o,(product A))) . a
then reconsider a9 = a as Element of I ;
thus f . a = const (o,(A . a9)) by A3
.= (const (o,(product A))) . a by A1, Th9 ; ::_thesis: verum
end;
set C = union { (Result (o,(A . i9))) where i9 is Element of I : verum } ;
const (o,(product A)) in Funcs (I,(union { (Result (o,(A . i9))) where i9 is Element of I : verum } )) by A1, Th8;
then ex g2 being Function st
( g2 = const (o,(product A)) & dom g2 = I & rng g2 c= union { (Result (o,(A . i9))) where i9 is Element of I : verum } ) by FUNCT_2:def_2;
hence f = const (o,(product A)) by A2, A4, FUNCT_1:2; ::_thesis: verum
end;
theorem Th11: :: PRALG_3:11
for S being non empty non void ManySortedSign
for U1, U2 being MSAlgebra over S
for o being OperSymbol of S
for e being Element of Args (o,U1) st e = {} & the_arity_of o = {} & Args (o,U1) <> {} & Args (o,U2) <> {} holds
for F being ManySortedFunction of U1,U2 holds F # e = {}
proof
let S be non empty non void ManySortedSign ; ::_thesis: for U1, U2 being MSAlgebra over S
for o being OperSymbol of S
for e being Element of Args (o,U1) st e = {} & the_arity_of o = {} & Args (o,U1) <> {} & Args (o,U2) <> {} holds
for F being ManySortedFunction of U1,U2 holds F # e = {}
let U1, U2 be MSAlgebra over S; ::_thesis: for o being OperSymbol of S
for e being Element of Args (o,U1) st e = {} & the_arity_of o = {} & Args (o,U1) <> {} & Args (o,U2) <> {} holds
for F being ManySortedFunction of U1,U2 holds F # e = {}
let o be OperSymbol of S; ::_thesis: for e being Element of Args (o,U1) st e = {} & the_arity_of o = {} & Args (o,U1) <> {} & Args (o,U2) <> {} holds
for F being ManySortedFunction of U1,U2 holds F # e = {}
let e be Element of Args (o,U1); ::_thesis: ( e = {} & the_arity_of o = {} & Args (o,U1) <> {} & Args (o,U2) <> {} implies for F being ManySortedFunction of U1,U2 holds F # e = {} )
assume that
A1: e = {} and
A2: the_arity_of o = {} and
A3: ( Args (o,U1) <> {} & Args (o,U2) <> {} ) ; ::_thesis: for F being ManySortedFunction of U1,U2 holds F # e = {}
reconsider e1 = e as Function by A1;
let F be ManySortedFunction of U1,U2; ::_thesis: F # e = {}
rng (the_arity_of o) = {} by A2;
then rng (the_arity_of o) c= dom F by XBOOLE_1:2;
then A4: dom (F * (the_arity_of o)) = dom (the_arity_of o) by RELAT_1:27
.= {} by A2 ;
then rng (F * (the_arity_of o)) = {} by RELAT_1:42;
then F * (the_arity_of o) is Function of {},{} by A4, FUNCT_2:1;
then A5: e1 in product (doms (F * (the_arity_of o))) by A1, CARD_3:10, FUNCT_6:23, TARSKI:def_1;
A6: F # e = (Frege (F * (the_arity_of o))) . e by A3, MSUALG_3:def_5
.= (F * (the_arity_of o)) .. e1 by A5, PRALG_2:def_2 ;
then reconsider fn = F # e as Function ;
A7: dom fn = {} by A4, A6, PRALG_1:def_17;
thus F # e = {} by A7; ::_thesis: verum
end;
begin
theorem Th12: :: PRALG_3:12
for S being non empty non void ManySortedSign
for o being OperSymbol of S
for U1, U2 being non-empty MSAlgebra over S
for F being ManySortedFunction of U1,U2
for x being Element of Args (o,U1) holds x in product (doms (F * (the_arity_of o)))
proof
let S be non empty non void ManySortedSign ; ::_thesis: for o being OperSymbol of S
for U1, U2 being non-empty MSAlgebra over S
for F being ManySortedFunction of U1,U2
for x being Element of Args (o,U1) holds x in product (doms (F * (the_arity_of o)))
let o be OperSymbol of S; ::_thesis: for U1, U2 being non-empty MSAlgebra over S
for F being ManySortedFunction of U1,U2
for x being Element of Args (o,U1) holds x in product (doms (F * (the_arity_of o)))
let U1, U2 be non-empty MSAlgebra over S; ::_thesis: for F being ManySortedFunction of U1,U2
for x being Element of Args (o,U1) holds x in product (doms (F * (the_arity_of o)))
let F be ManySortedFunction of U1,U2; ::_thesis: for x being Element of Args (o,U1) holds x in product (doms (F * (the_arity_of o)))
let x be Element of Args (o,U1); ::_thesis: x in product (doms (F * (the_arity_of o)))
x in Args (o,U1) ;
then A1: x in product ( the Sorts of U1 * (the_arity_of o)) by PRALG_2:3;
then A2: dom x = dom ( the Sorts of U1 * (the_arity_of o)) by CARD_3:9
.= dom (the_arity_of o) by PRALG_2:3 ;
dom F = the carrier of S by PARTFUN1:def_2;
then A3: rng (the_arity_of o) c= dom F ;
A4: now__::_thesis:_for_n_being_set_st_n_in_dom_(doms_(F_*_(the_arity_of_o)))_holds_
n_in_dom_x
let n be set ; ::_thesis: ( n in dom (doms (F * (the_arity_of o))) implies n in dom x )
assume n in dom (doms (F * (the_arity_of o))) ; ::_thesis: n in dom x
then n in (F * (the_arity_of o)) " (SubFuncs (rng (F * (the_arity_of o)))) by FUNCT_6:def_2;
then n in dom (F * (the_arity_of o)) by FUNCT_6:19;
hence n in dom x by A3, A2, RELAT_1:27; ::_thesis: verum
end;
A5: dom x = dom ( the Sorts of U1 * (the_arity_of o)) by A1, CARD_3:9;
A6: now__::_thesis:_for_n_being_set_st_n_in_dom_(doms_(F_*_(the_arity_of_o)))_holds_
x_._n_in_(doms_(F_*_(the_arity_of_o)))_._n
let n be set ; ::_thesis: ( n in dom (doms (F * (the_arity_of o))) implies x . n in (doms (F * (the_arity_of o))) . n )
assume A7: n in dom (doms (F * (the_arity_of o))) ; ::_thesis: x . n in (doms (F * (the_arity_of o))) . n
then A8: n in dom (the_arity_of o) by A2, A4;
then (the_arity_of o) . n in rng (the_arity_of o) by FUNCT_1:def_3;
then reconsider s1 = (the_arity_of o) . n as Element of the carrier of S ;
A9: n in dom (F * (the_arity_of o)) by A3, A8, RELAT_1:27;
then (F * (the_arity_of o)) . n = F . s1 by FUNCT_1:12;
then A10: (doms (F * (the_arity_of o))) . n = dom (F . s1) by A9, FUNCT_6:22
.= the Sorts of U1 . s1 by FUNCT_2:def_1 ;
n in dom ( the Sorts of U1 * (the_arity_of o)) by A5, A4, A7;
then x . n in ( the Sorts of U1 * (the_arity_of o)) . n by A1, CARD_3:9;
hence x . n in (doms (F * (the_arity_of o))) . n by A5, A4, A7, A10, FUNCT_1:12; ::_thesis: verum
end;
now__::_thesis:_for_n_being_set_st_n_in_dom_x_holds_
n_in_dom_(doms_(F_*_(the_arity_of_o)))
let n be set ; ::_thesis: ( n in dom x implies n in dom (doms (F * (the_arity_of o))) )
assume n in dom x ; ::_thesis: n in dom (doms (F * (the_arity_of o)))
then A11: n in dom (F * (the_arity_of o)) by A3, A2, RELAT_1:27;
(F * (the_arity_of o)) . n is Function ;
then n in (F * (the_arity_of o)) " (SubFuncs (rng (F * (the_arity_of o)))) by A11, FUNCT_6:19;
hence n in dom (doms (F * (the_arity_of o))) by FUNCT_6:def_2; ::_thesis: verum
end;
then A12: dom x c= dom (doms (F * (the_arity_of o))) by TARSKI:def_3;
dom (doms (F * (the_arity_of o))) c= dom x by A4, TARSKI:def_3;
then dom x = dom (doms (F * (the_arity_of o))) by A12, XBOOLE_0:def_10;
hence x in product (doms (F * (the_arity_of o))) by A6, CARD_3:9; ::_thesis: verum
end;
theorem Th13: :: PRALG_3:13
for S being non empty non void ManySortedSign
for o being OperSymbol of S
for U1, U2 being non-empty MSAlgebra over S
for F being ManySortedFunction of U1,U2
for x being Element of Args (o,U1)
for n being set st n in dom (the_arity_of o) holds
(F # x) . n = (F . ((the_arity_of o) /. n)) . (x . n)
proof
let S be non empty non void ManySortedSign ; ::_thesis: for o being OperSymbol of S
for U1, U2 being non-empty MSAlgebra over S
for F being ManySortedFunction of U1,U2
for x being Element of Args (o,U1)
for n being set st n in dom (the_arity_of o) holds
(F # x) . n = (F . ((the_arity_of o) /. n)) . (x . n)
let o be OperSymbol of S; ::_thesis: for U1, U2 being non-empty MSAlgebra over S
for F being ManySortedFunction of U1,U2
for x being Element of Args (o,U1)
for n being set st n in dom (the_arity_of o) holds
(F # x) . n = (F . ((the_arity_of o) /. n)) . (x . n)
let U1, U2 be non-empty MSAlgebra over S; ::_thesis: for F being ManySortedFunction of U1,U2
for x being Element of Args (o,U1)
for n being set st n in dom (the_arity_of o) holds
(F # x) . n = (F . ((the_arity_of o) /. n)) . (x . n)
let F be ManySortedFunction of U1,U2; ::_thesis: for x being Element of Args (o,U1)
for n being set st n in dom (the_arity_of o) holds
(F # x) . n = (F . ((the_arity_of o) /. n)) . (x . n)
let x be Element of Args (o,U1); ::_thesis: for n being set st n in dom (the_arity_of o) holds
(F # x) . n = (F . ((the_arity_of o) /. n)) . (x . n)
let n be set ; ::_thesis: ( n in dom (the_arity_of o) implies (F # x) . n = (F . ((the_arity_of o) /. n)) . (x . n) )
assume A1: n in dom (the_arity_of o) ; ::_thesis: (F # x) . n = (F . ((the_arity_of o) /. n)) . (x . n)
dom F = the carrier of S by PARTFUN1:def_2;
then rng (the_arity_of o) c= dom F ;
then A2: n in dom (F * (the_arity_of o)) by A1, RELAT_1:27;
A3: x in product (doms (F * (the_arity_of o))) by Th12;
thus (F # x) . n = ((Frege (F * (the_arity_of o))) . x) . n by MSUALG_3:def_5
.= ((F * (the_arity_of o)) .. x) . n by A3, PRALG_2:def_2
.= ((F * (the_arity_of o)) . n) . (x . n) by A2, PRALG_1:def_17
.= (F . ((the_arity_of o) . n)) . (x . n) by A2, FUNCT_1:12
.= (F . ((the_arity_of o) /. n)) . (x . n) by A1, PARTFUN1:def_6 ; ::_thesis: verum
end;
theorem Th14: :: PRALG_3:14
for I being non empty set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S
for x being Element of Args (o,(product A)) holds x in Funcs ((dom (the_arity_of o)),(Funcs (I,(union { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } ))))
proof
let I be non empty set ; ::_thesis: for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S
for x being Element of Args (o,(product A)) holds x in Funcs ((dom (the_arity_of o)),(Funcs (I,(union { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } ))))
let S be non empty non void ManySortedSign ; ::_thesis: for A being MSAlgebra-Family of I,S
for o being OperSymbol of S
for x being Element of Args (o,(product A)) holds x in Funcs ((dom (the_arity_of o)),(Funcs (I,(union { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } ))))
let A be MSAlgebra-Family of I,S; ::_thesis: for o being OperSymbol of S
for x being Element of Args (o,(product A)) holds x in Funcs ((dom (the_arity_of o)),(Funcs (I,(union { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } ))))
let o be OperSymbol of S; ::_thesis: for x being Element of Args (o,(product A)) holds x in Funcs ((dom (the_arity_of o)),(Funcs (I,(union { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } ))))
let x be Element of Args (o,(product A)); ::_thesis: x in Funcs ((dom (the_arity_of o)),(Funcs (I,(union { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } ))))
set C = union { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } ;
consider x1 being Function such that
A1: x1 = x ;
x in Args (o,(product A)) ;
then A2: x in product ( the Sorts of (product A) * (the_arity_of o)) by PRALG_2:3;
dom (SORTS A) = the carrier of S by PARTFUN1:def_2;
then A3: rng (the_arity_of o) c= dom (SORTS A) ;
now__::_thesis:_for_c_being_set_st_c_in_rng_x1_holds_
c_in_Funcs_(I,(union__{__(_the_Sorts_of_(A_._i9)_._s9)_where_i9_is_Element_of_I,_s9_is_Element_of_the_carrier_of_S_:_verum__}__))
let c be set ; ::_thesis: ( c in rng x1 implies c in Funcs (I,(union { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } )) )
assume c in rng x1 ; ::_thesis: c in Funcs (I,(union { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } ))
then consider n being set such that
A4: n in dom x1 and
A5: x1 . n = c by FUNCT_1:def_3;
A6: n in dom ((SORTS A) * (the_arity_of o)) by A2, A1, A4, CARD_3:9;
then n in dom (the_arity_of o) by A3, RELAT_1:27;
then (the_arity_of o) . n in rng (the_arity_of o) by FUNCT_1:def_3;
then reconsider s1 = (the_arity_of o) . n as Element of the carrier of S ;
x1 . n in ((SORTS A) * (the_arity_of o)) . n by A2, A1, A6, CARD_3:9;
then x1 . n in (SORTS A) . s1 by A6, FUNCT_1:12;
then x1 . n in product (Carrier (A,s1)) by PRALG_2:def_10;
then consider g being Function such that
A7: g = x1 . n and
A8: dom g = dom (Carrier (A,s1)) and
A9: for i9 being set st i9 in dom (Carrier (A,s1)) holds
g . i9 in (Carrier (A,s1)) . i9 by CARD_3:def_5;
now__::_thesis:_for_c1_being_set_st_c1_in_rng_g_holds_
c1_in_union__{__(_the_Sorts_of_(A_._i9)_._s9)_where_i9_is_Element_of_I,_s9_is_Element_of_the_carrier_of_S_:_verum__}_
let c1 be set ; ::_thesis: ( c1 in rng g implies c1 in union { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } )
assume c1 in rng g ; ::_thesis: c1 in union { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum }
then consider i1 being set such that
A10: i1 in dom g and
A11: g . i1 = c1 by FUNCT_1:def_3;
reconsider i1 = i1 as Element of I by A8, A10;
ex U0 being MSAlgebra over S st
( U0 = A . i1 & (Carrier (A,s1)) . i1 = the Sorts of U0 . s1 ) by PRALG_2:def_9;
then A12: g . i1 in the Sorts of (A . i1) . s1 by A8, A9, A10;
the Sorts of (A . i1) . s1 in { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } ;
hence c1 in union { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } by A11, A12, TARSKI:def_4; ::_thesis: verum
end;
then A13: rng g c= union { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } by TARSKI:def_3;
dom g = I by A8, PARTFUN1:def_2;
hence c in Funcs (I,(union { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } )) by A5, A7, A13, FUNCT_2:def_2; ::_thesis: verum
end;
then A14: rng x1 c= Funcs (I,(union { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } )) by TARSKI:def_3;
dom x = dom ((SORTS A) * (the_arity_of o)) by A2, CARD_3:9
.= dom (the_arity_of o) by A3, RELAT_1:27 ;
hence x in Funcs ((dom (the_arity_of o)),(Funcs (I,(union { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } )))) by A1, A14, FUNCT_2:def_2; ::_thesis: verum
end;
theorem Th15: :: PRALG_3:15
for I being non empty set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S
for x being Element of Args (o,(product A))
for n being set st n in dom (the_arity_of o) holds
x . n in product (Carrier (A,((the_arity_of o) /. n)))
proof
let I be non empty set ; ::_thesis: for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S
for x being Element of Args (o,(product A))
for n being set st n in dom (the_arity_of o) holds
x . n in product (Carrier (A,((the_arity_of o) /. n)))
let S be non empty non void ManySortedSign ; ::_thesis: for A being MSAlgebra-Family of I,S
for o being OperSymbol of S
for x being Element of Args (o,(product A))
for n being set st n in dom (the_arity_of o) holds
x . n in product (Carrier (A,((the_arity_of o) /. n)))
let A be MSAlgebra-Family of I,S; ::_thesis: for o being OperSymbol of S
for x being Element of Args (o,(product A))
for n being set st n in dom (the_arity_of o) holds
x . n in product (Carrier (A,((the_arity_of o) /. n)))
let o be OperSymbol of S; ::_thesis: for x being Element of Args (o,(product A))
for n being set st n in dom (the_arity_of o) holds
x . n in product (Carrier (A,((the_arity_of o) /. n)))
let x be Element of Args (o,(product A)); ::_thesis: for n being set st n in dom (the_arity_of o) holds
x . n in product (Carrier (A,((the_arity_of o) /. n)))
let n be set ; ::_thesis: ( n in dom (the_arity_of o) implies x . n in product (Carrier (A,((the_arity_of o) /. n))) )
assume A1: n in dom (the_arity_of o) ; ::_thesis: x . n in product (Carrier (A,((the_arity_of o) /. n)))
dom (SORTS A) = the carrier of S by PARTFUN1:def_2;
then rng (the_arity_of o) c= dom (SORTS A) ;
then A2: n in dom ((SORTS A) * (the_arity_of o)) by A1, RELAT_1:27;
x in Args (o,(product A)) ;
then x in product ( the Sorts of (product A) * (the_arity_of o)) by PRALG_2:3;
then x . n in ((SORTS A) * (the_arity_of o)) . n by A2, CARD_3:9;
then x . n in (SORTS A) . ((the_arity_of o) . n) by A2, FUNCT_1:12;
then x . n in (SORTS A) . ((the_arity_of o) /. n) by A1, PARTFUN1:def_6;
hence x . n in product (Carrier (A,((the_arity_of o) /. n))) by PRALG_2:def_10; ::_thesis: verum
end;
theorem Th16: :: PRALG_3:16
for I being non empty set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S
for i being Element of I
for n being set st n in dom (the_arity_of o) holds
for s being SortSymbol of S st s = (the_arity_of o) . n holds
for y being Element of Args (o,(product A))
for g being Function st g = y . n holds
g . i in the Sorts of (A . i) . s
proof
let I be non empty set ; ::_thesis: for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S
for i being Element of I
for n being set st n in dom (the_arity_of o) holds
for s being SortSymbol of S st s = (the_arity_of o) . n holds
for y being Element of Args (o,(product A))
for g being Function st g = y . n holds
g . i in the Sorts of (A . i) . s
let S be non empty non void ManySortedSign ; ::_thesis: for A being MSAlgebra-Family of I,S
for o being OperSymbol of S
for i being Element of I
for n being set st n in dom (the_arity_of o) holds
for s being SortSymbol of S st s = (the_arity_of o) . n holds
for y being Element of Args (o,(product A))
for g being Function st g = y . n holds
g . i in the Sorts of (A . i) . s
let A be MSAlgebra-Family of I,S; ::_thesis: for o being OperSymbol of S
for i being Element of I
for n being set st n in dom (the_arity_of o) holds
for s being SortSymbol of S st s = (the_arity_of o) . n holds
for y being Element of Args (o,(product A))
for g being Function st g = y . n holds
g . i in the Sorts of (A . i) . s
let o be OperSymbol of S; ::_thesis: for i being Element of I
for n being set st n in dom (the_arity_of o) holds
for s being SortSymbol of S st s = (the_arity_of o) . n holds
for y being Element of Args (o,(product A))
for g being Function st g = y . n holds
g . i in the Sorts of (A . i) . s
let i be Element of I; ::_thesis: for n being set st n in dom (the_arity_of o) holds
for s being SortSymbol of S st s = (the_arity_of o) . n holds
for y being Element of Args (o,(product A))
for g being Function st g = y . n holds
g . i in the Sorts of (A . i) . s
let n be set ; ::_thesis: ( n in dom (the_arity_of o) implies for s being SortSymbol of S st s = (the_arity_of o) . n holds
for y being Element of Args (o,(product A))
for g being Function st g = y . n holds
g . i in the Sorts of (A . i) . s )
assume n in dom (the_arity_of o) ; ::_thesis: for s being SortSymbol of S st s = (the_arity_of o) . n holds
for y being Element of Args (o,(product A))
for g being Function st g = y . n holds
g . i in the Sorts of (A . i) . s
then A1: n in dom ( the Sorts of (product A) * (the_arity_of o)) by PRALG_2:3;
let s be SortSymbol of S; ::_thesis: ( s = (the_arity_of o) . n implies for y being Element of Args (o,(product A))
for g being Function st g = y . n holds
g . i in the Sorts of (A . i) . s )
assume A2: s = (the_arity_of o) . n ; ::_thesis: for y being Element of Args (o,(product A))
for g being Function st g = y . n holds
g . i in the Sorts of (A . i) . s
let y be Element of Args (o,(product A)); ::_thesis: for g being Function st g = y . n holds
g . i in the Sorts of (A . i) . s
y in Args (o,(product A)) ;
then A3: y in product ( the Sorts of (product A) * (the_arity_of o)) by PRALG_2:3;
let g be Function; ::_thesis: ( g = y . n implies g . i in the Sorts of (A . i) . s )
assume g = y . n ; ::_thesis: g . i in the Sorts of (A . i) . s
then g in ( the Sorts of (product A) * (the_arity_of o)) . n by A1, A3, CARD_3:9;
then g in the Sorts of (product A) . s by A2, A1, FUNCT_1:12;
then A4: g in product (Carrier (A,s)) by PRALG_2:def_10;
i in I ;
then A5: i in dom (Carrier (A,s)) by PARTFUN1:def_2;
ex U0 being MSAlgebra over S st
( U0 = A . i & (Carrier (A,s)) . i = the Sorts of U0 . s ) by PRALG_2:def_9;
hence g . i in the Sorts of (A . i) . s by A5, A4, CARD_3:9; ::_thesis: verum
end;
theorem Th17: :: PRALG_3:17
for I being non empty set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S
for y being Element of Args (o,(product A)) st the_arity_of o <> {} holds
commute y in product (doms (A ?. o))
proof
let I be non empty set ; ::_thesis: for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S
for y being Element of Args (o,(product A)) st the_arity_of o <> {} holds
commute y in product (doms (A ?. o))
let S be non empty non void ManySortedSign ; ::_thesis: for A being MSAlgebra-Family of I,S
for o being OperSymbol of S
for y being Element of Args (o,(product A)) st the_arity_of o <> {} holds
commute y in product (doms (A ?. o))
let A be MSAlgebra-Family of I,S; ::_thesis: for o being OperSymbol of S
for y being Element of Args (o,(product A)) st the_arity_of o <> {} holds
commute y in product (doms (A ?. o))
let o be OperSymbol of S; ::_thesis: for y being Element of Args (o,(product A)) st the_arity_of o <> {} holds
commute y in product (doms (A ?. o))
let y be Element of Args (o,(product A)); ::_thesis: ( the_arity_of o <> {} implies commute y in product (doms (A ?. o)) )
set D = union { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } ;
A1: y in Funcs ((dom (the_arity_of o)),(Funcs (I,(union { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } )))) by Th14;
assume the_arity_of o <> {} ; ::_thesis: commute y in product (doms (A ?. o))
then commute y in Funcs (I,(Funcs ((dom (the_arity_of o)),(union { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } )))) by A1, FUNCT_6:55;
then A2: ex f being Function st
( f = commute y & dom f = I & rng f c= Funcs ((dom (the_arity_of o)),(union { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } )) ) by FUNCT_2:def_2;
A3: now__::_thesis:_for_i1_being_set_st_i1_in_dom_(doms_(A_?._o))_holds_
(commute_y)_._i1_in_(doms_(A_?._o))_._i1
let i1 be set ; ::_thesis: ( i1 in dom (doms (A ?. o)) implies (commute y) . i1 in (doms (A ?. o)) . i1 )
assume i1 in dom (doms (A ?. o)) ; ::_thesis: (commute y) . i1 in (doms (A ?. o)) . i1
then reconsider ii = i1 as Element of I by PRALG_2:11;
A4: now__::_thesis:_for_n_being_set_st_n_in_dom_(_the_Sorts_of_(A_._ii)_*_(the_arity_of_o))_holds_
((commute_y)_._ii)_._n_in_(_the_Sorts_of_(A_._ii)_*_(the_arity_of_o))_._n
let n be set ; ::_thesis: ( n in dom ( the Sorts of (A . ii) * (the_arity_of o)) implies ((commute y) . ii) . n in ( the Sorts of (A . ii) * (the_arity_of o)) . n )
assume A5: n in dom ( the Sorts of (A . ii) * (the_arity_of o)) ; ::_thesis: ((commute y) . ii) . n in ( the Sorts of (A . ii) * (the_arity_of o)) . n
then A6: n in dom (the_arity_of o) by PRALG_2:3;
then (the_arity_of o) . n in rng (the_arity_of o) by FUNCT_1:def_3;
then reconsider s1 = (the_arity_of o) . n as SortSymbol of S ;
A7: ex ff being Function st
( ff = y & dom ff = dom (the_arity_of o) & rng ff c= Funcs (I,(union { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } )) ) by A1, FUNCT_2:def_2;
then n in dom y by A5, PRALG_2:3;
then y . n in rng y by FUNCT_1:def_3;
then consider g being Function such that
A8: g = y . n and
dom g = I and
rng g c= union { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } by A7, FUNCT_2:def_2;
( ((commute y) . ii) . n = g . ii & g . ii in the Sorts of (A . ii) . s1 ) by A1, A6, A8, Th16, FUNCT_6:56;
hence ((commute y) . ii) . n in ( the Sorts of (A . ii) * (the_arity_of o)) . n by A5, FUNCT_1:12; ::_thesis: verum
end;
(commute y) . ii in rng (commute y) by A2, FUNCT_1:def_3;
then ex h being Function st
( h = (commute y) . ii & dom h = dom (the_arity_of o) & rng h c= union { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } ) by A2, FUNCT_2:def_2;
then dom ((commute y) . ii) = dom ( the Sorts of (A . ii) * (the_arity_of o)) by PRALG_2:3;
then (commute y) . ii in product ( the Sorts of (A . ii) * (the_arity_of o)) by A4, CARD_3:9;
then (commute y) . ii in Args (o,(A . ii)) by PRALG_2:3;
hence (commute y) . i1 in (doms (A ?. o)) . i1 by PRALG_2:11; ::_thesis: verum
end;
dom (commute y) = dom (doms (A ?. o)) by A2, PRALG_2:11;
hence commute y in product (doms (A ?. o)) by A3, CARD_3:9; ::_thesis: verum
end;
theorem Th18: :: PRALG_3:18
for I being non empty set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S
for y being Element of Args (o,(product A)) st the_arity_of o <> {} holds
y in dom (Commute (Frege (A ?. o)))
proof
let I be non empty set ; ::_thesis: for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S
for y being Element of Args (o,(product A)) st the_arity_of o <> {} holds
y in dom (Commute (Frege (A ?. o)))
let S be non empty non void ManySortedSign ; ::_thesis: for A being MSAlgebra-Family of I,S
for o being OperSymbol of S
for y being Element of Args (o,(product A)) st the_arity_of o <> {} holds
y in dom (Commute (Frege (A ?. o)))
let A be MSAlgebra-Family of I,S; ::_thesis: for o being OperSymbol of S
for y being Element of Args (o,(product A)) st the_arity_of o <> {} holds
y in dom (Commute (Frege (A ?. o)))
let o be OperSymbol of S; ::_thesis: for y being Element of Args (o,(product A)) st the_arity_of o <> {} holds
y in dom (Commute (Frege (A ?. o)))
let y be Element of Args (o,(product A)); ::_thesis: ( the_arity_of o <> {} implies y in dom (Commute (Frege (A ?. o))) )
set D = union { ( the Sorts of (A . ii) . ss) where ii is Element of I, ss is Element of the carrier of S : verum } ;
assume A1: the_arity_of o <> {} ; ::_thesis: y in dom (Commute (Frege (A ?. o)))
then commute y in product (doms (A ?. o)) by Th17;
then A2: commute y in dom (Frege (A ?. o)) by PARTFUN1:def_2;
y in Funcs ((dom (the_arity_of o)),(Funcs (I,(union { ( the Sorts of (A . ii) . ss) where ii is Element of I, ss is Element of the carrier of S : verum } )))) by Th14;
then y = commute (commute y) by A1, FUNCT_6:57;
hence y in dom (Commute (Frege (A ?. o))) by A2, PRALG_2:def_1; ::_thesis: verum
end;
theorem Th19: :: PRALG_3:19
for I being set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S
for x being Element of Args (o,(product A)) holds (Den (o,(product A))) . x in product (Carrier (A,(the_result_sort_of o)))
proof
let I be set ; ::_thesis: for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S
for x being Element of Args (o,(product A)) holds (Den (o,(product A))) . x in product (Carrier (A,(the_result_sort_of o)))
let S be non empty non void ManySortedSign ; ::_thesis: for A being MSAlgebra-Family of I,S
for o being OperSymbol of S
for x being Element of Args (o,(product A)) holds (Den (o,(product A))) . x in product (Carrier (A,(the_result_sort_of o)))
let A be MSAlgebra-Family of I,S; ::_thesis: for o being OperSymbol of S
for x being Element of Args (o,(product A)) holds (Den (o,(product A))) . x in product (Carrier (A,(the_result_sort_of o)))
let o be OperSymbol of S; ::_thesis: for x being Element of Args (o,(product A)) holds (Den (o,(product A))) . x in product (Carrier (A,(the_result_sort_of o)))
let x be Element of Args (o,(product A)); ::_thesis: (Den (o,(product A))) . x in product (Carrier (A,(the_result_sort_of o)))
Result (o,(product A)) = (SORTS A) . (the_result_sort_of o) by PRALG_2:3
.= product (Carrier (A,(the_result_sort_of o))) by PRALG_2:def_10 ;
hence (Den (o,(product A))) . x in product (Carrier (A,(the_result_sort_of o))) ; ::_thesis: verum
end;
theorem Th20: :: PRALG_3:20
for I being non empty set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for i being Element of I
for o being OperSymbol of S st the_arity_of o <> {} holds
for U1 being non-empty MSAlgebra over S
for x being Element of Args (o,(product A)) holds (commute x) . i is Element of Args (o,(A . i))
proof
let I be non empty set ; ::_thesis: for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for i being Element of I
for o being OperSymbol of S st the_arity_of o <> {} holds
for U1 being non-empty MSAlgebra over S
for x being Element of Args (o,(product A)) holds (commute x) . i is Element of Args (o,(A . i))
let S be non empty non void ManySortedSign ; ::_thesis: for A being MSAlgebra-Family of I,S
for i being Element of I
for o being OperSymbol of S st the_arity_of o <> {} holds
for U1 being non-empty MSAlgebra over S
for x being Element of Args (o,(product A)) holds (commute x) . i is Element of Args (o,(A . i))
let A be MSAlgebra-Family of I,S; ::_thesis: for i being Element of I
for o being OperSymbol of S st the_arity_of o <> {} holds
for U1 being non-empty MSAlgebra over S
for x being Element of Args (o,(product A)) holds (commute x) . i is Element of Args (o,(A . i))
let i be Element of I; ::_thesis: for o being OperSymbol of S st the_arity_of o <> {} holds
for U1 being non-empty MSAlgebra over S
for x being Element of Args (o,(product A)) holds (commute x) . i is Element of Args (o,(A . i))
let o be OperSymbol of S; ::_thesis: ( the_arity_of o <> {} implies for U1 being non-empty MSAlgebra over S
for x being Element of Args (o,(product A)) holds (commute x) . i is Element of Args (o,(A . i)) )
assume A1: the_arity_of o <> {} ; ::_thesis: for U1 being non-empty MSAlgebra over S
for x being Element of Args (o,(product A)) holds (commute x) . i is Element of Args (o,(A . i))
let U1 be non-empty MSAlgebra over S; ::_thesis: for x being Element of Args (o,(product A)) holds (commute x) . i is Element of Args (o,(A . i))
let x be Element of Args (o,(product A)); ::_thesis: (commute x) . i is Element of Args (o,(A . i))
i in I ;
then A2: i in dom (doms (A ?. o)) by PRALG_2:11;
commute x in product (doms (A ?. o)) by A1, Th17;
then (commute x) . i in (doms (A ?. o)) . i by A2, CARD_3:9;
hence (commute x) . i is Element of Args (o,(A . i)) by PRALG_2:11; ::_thesis: verum
end;
theorem Th21: :: PRALG_3:21
for I being non empty set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for i being Element of I
for o being OperSymbol of S
for x being Element of Args (o,(product A))
for n being set st n in dom (the_arity_of o) holds
for f being Function st f = x . n holds
((commute x) . i) . n = f . i
proof
let I be non empty set ; ::_thesis: for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for i being Element of I
for o being OperSymbol of S
for x being Element of Args (o,(product A))
for n being set st n in dom (the_arity_of o) holds
for f being Function st f = x . n holds
((commute x) . i) . n = f . i
let S be non empty non void ManySortedSign ; ::_thesis: for A being MSAlgebra-Family of I,S
for i being Element of I
for o being OperSymbol of S
for x being Element of Args (o,(product A))
for n being set st n in dom (the_arity_of o) holds
for f being Function st f = x . n holds
((commute x) . i) . n = f . i
let A be MSAlgebra-Family of I,S; ::_thesis: for i being Element of I
for o being OperSymbol of S
for x being Element of Args (o,(product A))
for n being set st n in dom (the_arity_of o) holds
for f being Function st f = x . n holds
((commute x) . i) . n = f . i
let i be Element of I; ::_thesis: for o being OperSymbol of S
for x being Element of Args (o,(product A))
for n being set st n in dom (the_arity_of o) holds
for f being Function st f = x . n holds
((commute x) . i) . n = f . i
let o be OperSymbol of S; ::_thesis: for x being Element of Args (o,(product A))
for n being set st n in dom (the_arity_of o) holds
for f being Function st f = x . n holds
((commute x) . i) . n = f . i
let x be Element of Args (o,(product A)); ::_thesis: for n being set st n in dom (the_arity_of o) holds
for f being Function st f = x . n holds
((commute x) . i) . n = f . i
let n be set ; ::_thesis: ( n in dom (the_arity_of o) implies for f being Function st f = x . n holds
((commute x) . i) . n = f . i )
assume A1: n in dom (the_arity_of o) ; ::_thesis: for f being Function st f = x . n holds
((commute x) . i) . n = f . i
set C = union { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } ;
A2: x in Funcs ((dom (the_arity_of o)),(Funcs (I,(union { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } )))) by Th14;
let g be Function; ::_thesis: ( g = x . n implies ((commute x) . i) . n = g . i )
assume g = x . n ; ::_thesis: ((commute x) . i) . n = g . i
hence ((commute x) . i) . n = g . i by A1, A2, FUNCT_6:56; ::_thesis: verum
end;
theorem Th22: :: PRALG_3:22
for I being non empty set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S st the_arity_of o <> {} holds
for y being Element of Args (o,(product A))
for i9 being Element of I
for g being Function st g = (Den (o,(product A))) . y holds
g . i9 = (Den (o,(A . i9))) . ((commute y) . i9)
proof
let I be non empty set ; ::_thesis: for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S st the_arity_of o <> {} holds
for y being Element of Args (o,(product A))
for i9 being Element of I
for g being Function st g = (Den (o,(product A))) . y holds
g . i9 = (Den (o,(A . i9))) . ((commute y) . i9)
let S be non empty non void ManySortedSign ; ::_thesis: for A being MSAlgebra-Family of I,S
for o being OperSymbol of S st the_arity_of o <> {} holds
for y being Element of Args (o,(product A))
for i9 being Element of I
for g being Function st g = (Den (o,(product A))) . y holds
g . i9 = (Den (o,(A . i9))) . ((commute y) . i9)
let A be MSAlgebra-Family of I,S; ::_thesis: for o being OperSymbol of S st the_arity_of o <> {} holds
for y being Element of Args (o,(product A))
for i9 being Element of I
for g being Function st g = (Den (o,(product A))) . y holds
g . i9 = (Den (o,(A . i9))) . ((commute y) . i9)
let o be OperSymbol of S; ::_thesis: ( the_arity_of o <> {} implies for y being Element of Args (o,(product A))
for i9 being Element of I
for g being Function st g = (Den (o,(product A))) . y holds
g . i9 = (Den (o,(A . i9))) . ((commute y) . i9) )
assume A1: the_arity_of o <> {} ; ::_thesis: for y being Element of Args (o,(product A))
for i9 being Element of I
for g being Function st g = (Den (o,(product A))) . y holds
g . i9 = (Den (o,(A . i9))) . ((commute y) . i9)
let y be Element of Args (o,(product A)); ::_thesis: for i9 being Element of I
for g being Function st g = (Den (o,(product A))) . y holds
g . i9 = (Den (o,(A . i9))) . ((commute y) . i9)
let i9 be Element of I; ::_thesis: for g being Function st g = (Den (o,(product A))) . y holds
g . i9 = (Den (o,(A . i9))) . ((commute y) . i9)
A2: y in dom (Commute (Frege (A ?. o))) by A1, Th18;
A3: commute y in product (doms (A ?. o)) by A1, Th17;
A4: Den (o,(product A)) = (OPS A) . o by MSUALG_1:def_6
.= IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o)))) by PRALG_2:def_13
.= Commute (Frege (A ?. o)) by A1, FUNCOP_1:def_8 ;
A5: dom (A ?. o) = I by PARTFUN1:def_2;
let g be Function; ::_thesis: ( g = (Den (o,(product A))) . y implies g . i9 = (Den (o,(A . i9))) . ((commute y) . i9) )
assume g = (Den (o,(product A))) . y ; ::_thesis: g . i9 = (Den (o,(A . i9))) . ((commute y) . i9)
then g = (Frege (A ?. o)) . (commute y) by A4, A2, PRALG_2:def_1
.= (A ?. o) .. (commute y) by A3, PRALG_2:def_2 ;
then g . i9 = ((A ?. o) . i9) . ((commute y) . i9) by A5, PRALG_1:def_17
.= (Den (o,(A . i9))) . ((commute y) . i9) by PRALG_2:7 ;
hence g . i9 = (Den (o,(A . i9))) . ((commute y) . i9) ; ::_thesis: verum
end;
begin
definition
let I be non empty set ;
let S be non empty non void ManySortedSign ;
let A be MSAlgebra-Family of I,S;
let i be Element of I;
func proj (A,i) -> ManySortedFunction of (product A),(A . i) means :Def2: :: PRALG_3:def 2
for s being Element of S holds it . s = proj ((Carrier (A,s)),i);
existence
ex b1 being ManySortedFunction of (product A),(A . i) st
for s being Element of S holds b1 . s = proj ((Carrier (A,s)),i)
proof
deffunc H1( Element of S) -> set = proj ((Carrier (A,$1)),i);
consider F being ManySortedSet of the carrier of S such that
A1: for s being Element of S holds F . s = H1(s) from PBOOLE:sch_5();
F is ManySortedFunction of (product A),(A . i)
proof
let s be set ; :: according to PBOOLE:def_15 ::_thesis: ( not s in the carrier of S or F . s is Element of K10(K11(( the Sorts of (product A) . s),( the Sorts of (A . i) . s))) )
assume A2: s in the carrier of S ; ::_thesis: F . s is Element of K10(K11(( the Sorts of (product A) . s),( the Sorts of (A . i) . s)))
F . s is Function of ( the Sorts of (product A) . s),( the Sorts of (A . i) . s)
proof
reconsider s9 = s as Element of S by A2;
F . s = proj ((Carrier (A,s9)),i) by A1;
then reconsider F9 = F . s as Function ;
A3: rng F9 c= the Sorts of (A . i) . s
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng F9 or y in the Sorts of (A . i) . s )
A4: ( dom (Carrier (A,s9)) = I & ex U0 being MSAlgebra over S st
( U0 = A . i & (Carrier (A,s9)) . i = the Sorts of U0 . s9 ) ) by PARTFUN1:def_2, PRALG_2:def_9;
assume y in rng F9 ; ::_thesis: y in the Sorts of (A . i) . s
then y in rng (proj ((Carrier (A,s9)),i)) by A1;
then consider x1 being set such that
A5: x1 in dom (proj ((Carrier (A,s9)),i)) and
A6: y = (proj ((Carrier (A,s9)),i)) . x1 by FUNCT_1:def_3;
A7: x1 in product (Carrier (A,s9)) by A5;
then reconsider x1 = x1 as Function ;
y = x1 . i by A5, A6, CARD_3:def_16;
hence y in the Sorts of (A . i) . s by A7, A4, CARD_3:9; ::_thesis: verum
end;
dom F9 = dom (proj ((Carrier (A,s9)),i)) by A1
.= product (Carrier (A,s9)) by CARD_3:def_16
.= the Sorts of (product A) . s by PRALG_2:def_10 ;
hence F . s is Function of ( the Sorts of (product A) . s),( the Sorts of (A . i) . s) by A2, A3, FUNCT_2:def_1, RELSET_1:4; ::_thesis: verum
end;
hence F . s is Element of K10(K11(( the Sorts of (product A) . s),( the Sorts of (A . i) . s))) ; ::_thesis: verum
end;
then reconsider F9 = F as ManySortedFunction of (product A),(A . i) ;
take F9 ; ::_thesis: for s being Element of S holds F9 . s = proj ((Carrier (A,s)),i)
thus for s being Element of S holds F9 . s = proj ((Carrier (A,s)),i) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being ManySortedFunction of (product A),(A . i) st ( for s being Element of S holds b1 . s = proj ((Carrier (A,s)),i) ) & ( for s being Element of S holds b2 . s = proj ((Carrier (A,s)),i) ) holds
b1 = b2
proof
let F, G be ManySortedFunction of (product A),(A . i); ::_thesis: ( ( for s being Element of S holds F . s = proj ((Carrier (A,s)),i) ) & ( for s being Element of S holds G . s = proj ((Carrier (A,s)),i) ) implies F = G )
assume that
A8: for s being Element of S holds F . s = proj ((Carrier (A,s)),i) and
A9: for s being Element of S holds G . s = proj ((Carrier (A,s)),i) ; ::_thesis: F = G
now__::_thesis:_for_s9_being_set_st_s9_in_the_carrier_of_S_holds_
F_._s9_=_G_._s9
let s9 be set ; ::_thesis: ( s9 in the carrier of S implies F . s9 = G . s9 )
assume s9 in the carrier of S ; ::_thesis: F . s9 = G . s9
then reconsider s99 = s9 as Element of S ;
thus F . s9 = proj ((Carrier (A,s99)),i) by A8
.= G . s9 by A9 ; ::_thesis: verum
end;
hence F = G by PBOOLE:3; ::_thesis: verum
end;
end;
:: deftheorem Def2 defines proj PRALG_3:def_2_:_
for I being non empty set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for i being Element of I
for b5 being ManySortedFunction of (product A),(A . i) holds
( b5 = proj (A,i) iff for s being Element of S holds b5 . s = proj ((Carrier (A,s)),i) );
theorem Th23: :: PRALG_3:23
for I being non empty set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S
for x being Element of Args (o,(product A)) st the_arity_of o <> {} holds
for i being Element of I holds (proj (A,i)) # x = (commute x) . i
proof
let I be non empty set ; ::_thesis: for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S
for x being Element of Args (o,(product A)) st the_arity_of o <> {} holds
for i being Element of I holds (proj (A,i)) # x = (commute x) . i
let S be non empty non void ManySortedSign ; ::_thesis: for A being MSAlgebra-Family of I,S
for o being OperSymbol of S
for x being Element of Args (o,(product A)) st the_arity_of o <> {} holds
for i being Element of I holds (proj (A,i)) # x = (commute x) . i
let A be MSAlgebra-Family of I,S; ::_thesis: for o being OperSymbol of S
for x being Element of Args (o,(product A)) st the_arity_of o <> {} holds
for i being Element of I holds (proj (A,i)) # x = (commute x) . i
let o be OperSymbol of S; ::_thesis: for x being Element of Args (o,(product A)) st the_arity_of o <> {} holds
for i being Element of I holds (proj (A,i)) # x = (commute x) . i
let x be Element of Args (o,(product A)); ::_thesis: ( the_arity_of o <> {} implies for i being Element of I holds (proj (A,i)) # x = (commute x) . i )
assume A1: the_arity_of o <> {} ; ::_thesis: for i being Element of I holds (proj (A,i)) # x = (commute x) . i
set C = union { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } ;
let i be Element of I; ::_thesis: (proj (A,i)) # x = (commute x) . i
A2: x in Funcs ((dom (the_arity_of o)),(Funcs (I,(union { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } )))) by Th14;
then A3: commute x in Funcs (I,(Funcs ((dom (the_arity_of o)),(union { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } )))) by A1, FUNCT_6:55;
then dom (commute x) = I by FUNCT_2:92;
then A4: (commute x) . i in rng (commute x) by FUNCT_1:def_3;
A5: now__::_thesis:_for_n_being_set_st_n_in_dom_(the_arity_of_o)_holds_
((proj_(A,i))_#_x)_._n_=_((commute_x)_._i)_._n
A6: rng x c= Funcs (I,(union { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } )) by A2, FUNCT_2:92;
let n be set ; ::_thesis: ( n in dom (the_arity_of o) implies ((proj (A,i)) # x) . n = ((commute x) . i) . n )
assume A7: n in dom (the_arity_of o) ; ::_thesis: ((proj (A,i)) # x) . n = ((commute x) . i) . n
x . n in product (Carrier (A,((the_arity_of o) /. n))) by A7, Th15;
then A8: x . n in dom (proj ((Carrier (A,((the_arity_of o) /. n))),i)) by CARD_3:def_16;
n in dom x by A2, A7, FUNCT_2:92;
then x . n in rng x by FUNCT_1:def_3;
then consider g being Function such that
A9: g = x . n and
dom g = I and
rng g c= union { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } by A6, FUNCT_2:def_2;
thus ((proj (A,i)) # x) . n = ((proj (A,i)) . ((the_arity_of o) /. n)) . (x . n) by A7, Th13
.= (proj ((Carrier (A,((the_arity_of o) /. n))),i)) . (x . n) by Def2
.= g . i by A9, A8, CARD_3:def_16
.= ((commute x) . i) . n by A2, A7, A9, FUNCT_6:56 ; ::_thesis: verum
end;
A10: x in product (doms ((proj (A,i)) * (the_arity_of o))) by Th12;
rng (commute x) c= Funcs ((dom (the_arity_of o)),(union { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } )) by A3, FUNCT_2:92;
then A11: dom ((commute x) . i) = dom (the_arity_of o) by A4, FUNCT_2:92;
dom (proj (A,i)) = the carrier of S by PARTFUN1:def_2;
then A12: rng (the_arity_of o) c= dom (proj (A,i)) ;
dom ((proj (A,i)) # x) = dom ((Frege ((proj (A,i)) * (the_arity_of o))) . x) by MSUALG_3:def_5
.= dom (((proj (A,i)) * (the_arity_of o)) .. x) by A10, PRALG_2:def_2
.= dom ((proj (A,i)) * (the_arity_of o)) by PRALG_1:def_17
.= dom (the_arity_of o) by A12, RELAT_1:27 ;
hence (proj (A,i)) # x = (commute x) . i by A11, A5, FUNCT_1:2; ::_thesis: verum
end;
theorem :: PRALG_3:24
for I being non empty set
for S being non empty non void ManySortedSign
for i being Element of I
for A being MSAlgebra-Family of I,S holds proj (A,i) is_homomorphism product A,A . i
proof
let I be non empty set ; ::_thesis: for S being non empty non void ManySortedSign
for i being Element of I
for A being MSAlgebra-Family of I,S holds proj (A,i) is_homomorphism product A,A . i
let S be non empty non void ManySortedSign ; ::_thesis: for i being Element of I
for A being MSAlgebra-Family of I,S holds proj (A,i) is_homomorphism product A,A . i
let i be Element of I; ::_thesis: for A being MSAlgebra-Family of I,S holds proj (A,i) is_homomorphism product A,A . i
let A be MSAlgebra-Family of I,S; ::_thesis: proj (A,i) is_homomorphism product A,A . i
thus proj (A,i) is_homomorphism product A,A . i ::_thesis: verum
proof
let o be OperSymbol of S; :: according to MSUALG_3:def_7 ::_thesis: ( Args (o,(product A)) = {} or for b1 being Element of Args (o,(product A)) holds ((proj (A,i)) . (the_result_sort_of o)) . ((Den (o,(product A))) . b1) = (Den (o,(A . i))) . ((proj (A,i)) # b1) )
assume Args (o,(product A)) <> {} ; ::_thesis: for b1 being Element of Args (o,(product A)) holds ((proj (A,i)) . (the_result_sort_of o)) . ((Den (o,(product A))) . b1) = (Den (o,(A . i))) . ((proj (A,i)) # b1)
let x be Element of Args (o,(product A)); ::_thesis: ((proj (A,i)) . (the_result_sort_of o)) . ((Den (o,(product A))) . x) = (Den (o,(A . i))) . ((proj (A,i)) # x)
set F = proj (A,i);
set s = the_result_sort_of o;
o in the carrier' of S ;
then A1: o in dom the ResultSort of S by FUNCT_2:def_1;
A2: Result (o,(product A)) = ( the Sorts of (product A) * the ResultSort of S) . o by MSUALG_1:def_5
.= the Sorts of (product A) . ( the ResultSort of S . o) by A1, FUNCT_1:13
.= (SORTS A) . (the_result_sort_of o) by MSUALG_1:def_2
.= product (Carrier (A,(the_result_sort_of o))) by PRALG_2:def_10 ;
thus ((proj (A,i)) . (the_result_sort_of o)) . ((Den (o,(product A))) . x) = (Den (o,(A . i))) . ((proj (A,i)) # x) ::_thesis: verum
proof
percases ( the_arity_of o = {} or the_arity_of o <> {} ) ;
supposeA3: the_arity_of o = {} ; ::_thesis: ((proj (A,i)) . (the_result_sort_of o)) . ((Den (o,(product A))) . x) = (Den (o,(A . i))) . ((proj (A,i)) # x)
then const (o,(product A)) in product (Carrier (A,(the_result_sort_of o))) by A2, Th5;
then A4: const (o,(product A)) in dom (proj ((Carrier (A,(the_result_sort_of o))),i)) by CARD_3:def_16;
A5: Args (o,(product A)) = {{}} by A3, PRALG_2:4;
then A6: x = {} by TARSKI:def_1;
((proj (A,i)) . (the_result_sort_of o)) . ((Den (o,(product A))) . x) = ((proj (A,i)) . (the_result_sort_of o)) . (const (o,(product A))) by A5, TARSKI:def_1
.= (proj ((Carrier (A,(the_result_sort_of o))),i)) . (const (o,(product A))) by Def2
.= (const (o,(product A))) . i by A4, CARD_3:def_16
.= const (o,(A . i)) by A3, Th9
.= (Den (o,(A . i))) . ((proj (A,i)) # x) by A3, A6, Th11 ;
hence ((proj (A,i)) . (the_result_sort_of o)) . ((Den (o,(product A))) . x) = (Den (o,(A . i))) . ((proj (A,i)) # x) ; ::_thesis: verum
end;
supposeA7: the_arity_of o <> {} ; ::_thesis: ((proj (A,i)) . (the_result_sort_of o)) . ((Den (o,(product A))) . x) = (Den (o,(A . i))) . ((proj (A,i)) # x)
reconsider D = (Den (o,(product A))) . x as Function by A2;
(Den (o,(product A))) . x in product (Carrier (A,(the_result_sort_of o))) by A2;
then A8: (Den (o,(product A))) . x in dom (proj ((Carrier (A,(the_result_sort_of o))),i)) by CARD_3:def_16;
((proj (A,i)) . (the_result_sort_of o)) . ((Den (o,(product A))) . x) = (proj ((Carrier (A,(the_result_sort_of o))),i)) . ((Den (o,(product A))) . x) by Def2
.= D . i by A8, CARD_3:def_16
.= (Den (o,(A . i))) . ((commute x) . i) by A7, Th22
.= (Den (o,(A . i))) . ((proj (A,i)) # x) by A7, Th23 ;
hence ((proj (A,i)) . (the_result_sort_of o)) . ((Den (o,(product A))) . x) = (Den (o,(A . i))) . ((proj (A,i)) # x) ; ::_thesis: verum
end;
end;
end;
end;
end;
theorem Th25: :: PRALG_3:25
for I being non empty set
for S being non empty non void ManySortedSign
for i being Element of I
for A being MSAlgebra-Family of I,S
for s being SortSymbol of S
for U1 being non-empty MSAlgebra over S
for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st
( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds
( F in Funcs (I,(Funcs ( the carrier of S, { ((F . i9) . s1) where s1 is SortSymbol of S, i9 is Element of I : verum } ))) & ((commute F) . s) . i = (F . i) . s )
proof
let I be non empty set ; ::_thesis: for S being non empty non void ManySortedSign
for i being Element of I
for A being MSAlgebra-Family of I,S
for s being SortSymbol of S
for U1 being non-empty MSAlgebra over S
for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st
( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds
( F in Funcs (I,(Funcs ( the carrier of S, { ((F . i9) . s1) where s1 is SortSymbol of S, i9 is Element of I : verum } ))) & ((commute F) . s) . i = (F . i) . s )
let S be non empty non void ManySortedSign ; ::_thesis: for i being Element of I
for A being MSAlgebra-Family of I,S
for s being SortSymbol of S
for U1 being non-empty MSAlgebra over S
for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st
( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds
( F in Funcs (I,(Funcs ( the carrier of S, { ((F . i9) . s1) where s1 is SortSymbol of S, i9 is Element of I : verum } ))) & ((commute F) . s) . i = (F . i) . s )
let i be Element of I; ::_thesis: for A being MSAlgebra-Family of I,S
for s being SortSymbol of S
for U1 being non-empty MSAlgebra over S
for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st
( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds
( F in Funcs (I,(Funcs ( the carrier of S, { ((F . i9) . s1) where s1 is SortSymbol of S, i9 is Element of I : verum } ))) & ((commute F) . s) . i = (F . i) . s )
let A be MSAlgebra-Family of I,S; ::_thesis: for s being SortSymbol of S
for U1 being non-empty MSAlgebra over S
for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st
( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds
( F in Funcs (I,(Funcs ( the carrier of S, { ((F . i9) . s1) where s1 is SortSymbol of S, i9 is Element of I : verum } ))) & ((commute F) . s) . i = (F . i) . s )
let s be SortSymbol of S; ::_thesis: for U1 being non-empty MSAlgebra over S
for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st
( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds
( F in Funcs (I,(Funcs ( the carrier of S, { ((F . i9) . s1) where s1 is SortSymbol of S, i9 is Element of I : verum } ))) & ((commute F) . s) . i = (F . i) . s )
let U1 be non-empty MSAlgebra over S; ::_thesis: for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st
( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds
( F in Funcs (I,(Funcs ( the carrier of S, { ((F . i9) . s1) where s1 is SortSymbol of S, i9 is Element of I : verum } ))) & ((commute F) . s) . i = (F . i) . s )
let F be ManySortedFunction of I; ::_thesis: ( ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st
( F1 = F . i & F1 is_homomorphism U1,A . i ) ) implies ( F in Funcs (I,(Funcs ( the carrier of S, { ((F . i9) . s1) where s1 is SortSymbol of S, i9 is Element of I : verum } ))) & ((commute F) . s) . i = (F . i) . s ) )
assume A1: for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st
( F1 = F . i & F1 is_homomorphism U1,A . i ) ; ::_thesis: ( F in Funcs (I,(Funcs ( the carrier of S, { ((F . i9) . s1) where s1 is SortSymbol of S, i9 is Element of I : verum } ))) & ((commute F) . s) . i = (F . i) . s )
set FS = { ((F . i9) . s1) where s1 is SortSymbol of S, i9 is Element of I : verum } ;
set CA = the carrier of S;
A2: rng F c= Funcs ( the carrier of S, { ((F . i9) . s1) where s1 is SortSymbol of S, i9 is Element of I : verum } )
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng F or x in Funcs ( the carrier of S, { ((F . i9) . s1) where s1 is SortSymbol of S, i9 is Element of I : verum } ) )
assume x in rng F ; ::_thesis: x in Funcs ( the carrier of S, { ((F . i9) . s1) where s1 is SortSymbol of S, i9 is Element of I : verum } )
then consider i9 being set such that
A3: i9 in dom F and
A4: F . i9 = x by FUNCT_1:def_3;
reconsider i1 = i9 as Element of I by A3;
consider F9 being ManySortedFunction of U1,(A . i1) such that
A5: F9 = F . i1 and
F9 is_homomorphism U1,A . i1 by A1;
A6: rng F9 c= { ((F . i9) . s1) where s1 is SortSymbol of S, i9 is Element of I : verum }
proof
let x9 be set ; :: according to TARSKI:def_3 ::_thesis: ( not x9 in rng F9 or x9 in { ((F . i9) . s1) where s1 is SortSymbol of S, i9 is Element of I : verum } )
assume x9 in rng F9 ; ::_thesis: x9 in { ((F . i9) . s1) where s1 is SortSymbol of S, i9 is Element of I : verum }
then consider s9 being set such that
A7: s9 in dom F9 and
A8: F9 . s9 = x9 by FUNCT_1:def_3;
s9 is SortSymbol of S by A7;
hence x9 in { ((F . i9) . s1) where s1 is SortSymbol of S, i9 is Element of I : verum } by A5, A8; ::_thesis: verum
end;
dom F9 = the carrier of S by PARTFUN1:def_2;
hence x in Funcs ( the carrier of S, { ((F . i9) . s1) where s1 is SortSymbol of S, i9 is Element of I : verum } ) by A4, A5, A6, FUNCT_2:def_2; ::_thesis: verum
end;
A9: dom F = I by PARTFUN1:def_2;
hence F in Funcs (I,(Funcs ( the carrier of S, { ((F . i9) . s1) where s1 is SortSymbol of S, i9 is Element of I : verum } ))) by A2, FUNCT_2:def_2; ::_thesis: ((commute F) . s) . i = (F . i) . s
F in Funcs (I,(Funcs ( the carrier of S, { ((F . i9) . s1) where s1 is SortSymbol of S, i9 is Element of I : verum } ))) by A9, A2, FUNCT_2:def_2;
hence ((commute F) . s) . i = (F . i) . s by FUNCT_6:56; ::_thesis: verum
end;
theorem Th26: :: PRALG_3:26
for I being non empty set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for s being SortSymbol of S
for U1 being non-empty MSAlgebra over S
for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st
( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds
(commute F) . s in Funcs (I,(Funcs (( the Sorts of U1 . s),(union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } ))))
proof
let I be non empty set ; ::_thesis: for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for s being SortSymbol of S
for U1 being non-empty MSAlgebra over S
for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st
( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds
(commute F) . s in Funcs (I,(Funcs (( the Sorts of U1 . s),(union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } ))))
let S be non empty non void ManySortedSign ; ::_thesis: for A being MSAlgebra-Family of I,S
for s being SortSymbol of S
for U1 being non-empty MSAlgebra over S
for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st
( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds
(commute F) . s in Funcs (I,(Funcs (( the Sorts of U1 . s),(union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } ))))
let A be MSAlgebra-Family of I,S; ::_thesis: for s being SortSymbol of S
for U1 being non-empty MSAlgebra over S
for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st
( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds
(commute F) . s in Funcs (I,(Funcs (( the Sorts of U1 . s),(union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } ))))
let s be SortSymbol of S; ::_thesis: for U1 being non-empty MSAlgebra over S
for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st
( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds
(commute F) . s in Funcs (I,(Funcs (( the Sorts of U1 . s),(union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } ))))
let U1 be non-empty MSAlgebra over S; ::_thesis: for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st
( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds
(commute F) . s in Funcs (I,(Funcs (( the Sorts of U1 . s),(union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } ))))
let F be ManySortedFunction of I; ::_thesis: ( ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st
( F1 = F . i & F1 is_homomorphism U1,A . i ) ) implies (commute F) . s in Funcs (I,(Funcs (( the Sorts of U1 . s),(union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } )))) )
assume A1: for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st
( F1 = F . i & F1 is_homomorphism U1,A . i ) ; ::_thesis: (commute F) . s in Funcs (I,(Funcs (( the Sorts of U1 . s),(union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } ))))
set SU = the Sorts of U1;
set CA = the carrier of S;
set SA = union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } ;
set SA9 = { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } ;
set FS = { ((F . i9) . s1) where s1 is SortSymbol of S, i9 is Element of I : verum } ;
F in Funcs (I,(Funcs ( the carrier of S, { ((F . i9) . s1) where s1 is SortSymbol of S, i9 is Element of I : verum } ))) by A1, Th25;
then commute F in Funcs ( the carrier of S,(Funcs (I, { ((F . i9) . s1) where s1 is SortSymbol of S, i9 is Element of I : verum } ))) by FUNCT_6:55;
then consider F9 being Function such that
A2: ( F9 = commute F & dom F9 = the carrier of S ) and
A3: rng F9 c= Funcs (I, { ((F . i9) . s1) where s1 is SortSymbol of S, i9 is Element of I : verum } ) by FUNCT_2:def_2;
(commute F) . s in rng F9 by A2, FUNCT_1:def_3;
then A4: ex F2 being Function st
( F2 = (commute F) . s & dom F2 = I & rng F2 c= { ((F . i9) . s1) where s1 is SortSymbol of S, i9 is Element of I : verum } ) by A3, FUNCT_2:def_2;
rng ((commute F) . s) c= Funcs (( the Sorts of U1 . s),(union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } ))
proof
let x9 be set ; :: according to TARSKI:def_3 ::_thesis: ( not x9 in rng ((commute F) . s) or x9 in Funcs (( the Sorts of U1 . s),(union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } )) )
assume x9 in rng ((commute F) . s) ; ::_thesis: x9 in Funcs (( the Sorts of U1 . s),(union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } ))
then consider i9 being set such that
A5: i9 in dom ((commute F) . s) and
A6: x9 = ((commute F) . s) . i9 by FUNCT_1:def_3;
reconsider i1 = i9 as Element of I by A4, A5;
consider F9 being ManySortedFunction of U1,(A . i1) such that
A7: F9 = F . i1 and
F9 is_homomorphism U1,A . i1 by A1;
the Sorts of (A . i1) . s c= union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum }
proof
A8: the Sorts of (A . i1) . s in { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } ;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in the Sorts of (A . i1) . s or y in union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } )
assume y in the Sorts of (A . i1) . s ; ::_thesis: y in union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum }
hence y in union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } by A8, TARSKI:def_4; ::_thesis: verum
end;
then A9: ( dom (F9 . s) = the Sorts of U1 . s & rng (F9 . s) c= union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } ) by FUNCT_2:def_1, XBOOLE_1:1;
x9 = F9 . s by A1, A6, A7, Th25;
hence x9 in Funcs (( the Sorts of U1 . s),(union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } )) by A9, FUNCT_2:def_2; ::_thesis: verum
end;
hence (commute F) . s in Funcs (I,(Funcs (( the Sorts of U1 . s),(union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } )))) by A4, FUNCT_2:def_2; ::_thesis: verum
end;
theorem Th27: :: PRALG_3:27
for I being non empty set
for S being non empty non void ManySortedSign
for i being Element of I
for A being MSAlgebra-Family of I,S
for s being SortSymbol of S
for U1 being non-empty MSAlgebra over S
for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st
( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds
for F9 being ManySortedFunction of U1,(A . i) st F9 = F . i holds
for x being set st x in the Sorts of U1 . s holds
for f being Function st f = (commute ((commute F) . s)) . x holds
f . i = (F9 . s) . x
proof
let I be non empty set ; ::_thesis: for S being non empty non void ManySortedSign
for i being Element of I
for A being MSAlgebra-Family of I,S
for s being SortSymbol of S
for U1 being non-empty MSAlgebra over S
for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st
( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds
for F9 being ManySortedFunction of U1,(A . i) st F9 = F . i holds
for x being set st x in the Sorts of U1 . s holds
for f being Function st f = (commute ((commute F) . s)) . x holds
f . i = (F9 . s) . x
let S be non empty non void ManySortedSign ; ::_thesis: for i being Element of I
for A being MSAlgebra-Family of I,S
for s being SortSymbol of S
for U1 being non-empty MSAlgebra over S
for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st
( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds
for F9 being ManySortedFunction of U1,(A . i) st F9 = F . i holds
for x being set st x in the Sorts of U1 . s holds
for f being Function st f = (commute ((commute F) . s)) . x holds
f . i = (F9 . s) . x
let i be Element of I; ::_thesis: for A being MSAlgebra-Family of I,S
for s being SortSymbol of S
for U1 being non-empty MSAlgebra over S
for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st
( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds
for F9 being ManySortedFunction of U1,(A . i) st F9 = F . i holds
for x being set st x in the Sorts of U1 . s holds
for f being Function st f = (commute ((commute F) . s)) . x holds
f . i = (F9 . s) . x
let A be MSAlgebra-Family of I,S; ::_thesis: for s being SortSymbol of S
for U1 being non-empty MSAlgebra over S
for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st
( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds
for F9 being ManySortedFunction of U1,(A . i) st F9 = F . i holds
for x being set st x in the Sorts of U1 . s holds
for f being Function st f = (commute ((commute F) . s)) . x holds
f . i = (F9 . s) . x
let s be SortSymbol of S; ::_thesis: for U1 being non-empty MSAlgebra over S
for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st
( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds
for F9 being ManySortedFunction of U1,(A . i) st F9 = F . i holds
for x being set st x in the Sorts of U1 . s holds
for f being Function st f = (commute ((commute F) . s)) . x holds
f . i = (F9 . s) . x
let U1 be non-empty MSAlgebra over S; ::_thesis: for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st
( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds
for F9 being ManySortedFunction of U1,(A . i) st F9 = F . i holds
for x being set st x in the Sorts of U1 . s holds
for f being Function st f = (commute ((commute F) . s)) . x holds
f . i = (F9 . s) . x
set SU = the Sorts of U1;
set SA = union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } ;
let F be ManySortedFunction of I; ::_thesis: ( ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st
( F1 = F . i & F1 is_homomorphism U1,A . i ) ) implies for F9 being ManySortedFunction of U1,(A . i) st F9 = F . i holds
for x being set st x in the Sorts of U1 . s holds
for f being Function st f = (commute ((commute F) . s)) . x holds
f . i = (F9 . s) . x )
assume A1: for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st
( F1 = F . i & F1 is_homomorphism U1,A . i ) ; ::_thesis: for F9 being ManySortedFunction of U1,(A . i) st F9 = F . i holds
for x being set st x in the Sorts of U1 . s holds
for f being Function st f = (commute ((commute F) . s)) . x holds
f . i = (F9 . s) . x
A2: (commute F) . s in Funcs (I,(Funcs (( the Sorts of U1 . s),(union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } )))) by A1, Th26;
then dom ((commute F) . s) = I by FUNCT_2:92;
then A3: ((commute F) . s) . i in rng ((commute F) . s) by FUNCT_1:def_3;
reconsider f9 = (commute F) . s as Function ;
rng ((commute F) . s) c= Funcs (( the Sorts of U1 . s),(union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } )) by A2, FUNCT_2:92;
then consider g being Function such that
A4: g = f9 . i and
dom g = the Sorts of U1 . s and
rng g c= union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } by A3, FUNCT_2:def_2;
let F9 be ManySortedFunction of U1,(A . i); ::_thesis: ( F9 = F . i implies for x being set st x in the Sorts of U1 . s holds
for f being Function st f = (commute ((commute F) . s)) . x holds
f . i = (F9 . s) . x )
assume A5: F9 = F . i ; ::_thesis: for x being set st x in the Sorts of U1 . s holds
for f being Function st f = (commute ((commute F) . s)) . x holds
f . i = (F9 . s) . x
let x1 be set ; ::_thesis: ( x1 in the Sorts of U1 . s implies for f being Function st f = (commute ((commute F) . s)) . x1 holds
f . i = (F9 . s) . x1 )
assume A6: x1 in the Sorts of U1 . s ; ::_thesis: for f being Function st f = (commute ((commute F) . s)) . x1 holds
f . i = (F9 . s) . x1
let f be Function; ::_thesis: ( f = (commute ((commute F) . s)) . x1 implies f . i = (F9 . s) . x1 )
assume A7: f = (commute ((commute F) . s)) . x1 ; ::_thesis: f . i = (F9 . s) . x1
g = F9 . s by A1, A5, A4, Th25;
hence f . i = (F9 . s) . x1 by A6, A7, A2, A4, FUNCT_6:56; ::_thesis: verum
end;
theorem Th28: :: PRALG_3:28
for I being non empty set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for s being SortSymbol of S
for U1 being non-empty MSAlgebra over S
for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st
( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds
for x being set st x in the Sorts of U1 . s holds
(commute ((commute F) . s)) . x in product (Carrier (A,s))
proof
let I be non empty set ; ::_thesis: for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for s being SortSymbol of S
for U1 being non-empty MSAlgebra over S
for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st
( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds
for x being set st x in the Sorts of U1 . s holds
(commute ((commute F) . s)) . x in product (Carrier (A,s))
let S be non empty non void ManySortedSign ; ::_thesis: for A being MSAlgebra-Family of I,S
for s being SortSymbol of S
for U1 being non-empty MSAlgebra over S
for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st
( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds
for x being set st x in the Sorts of U1 . s holds
(commute ((commute F) . s)) . x in product (Carrier (A,s))
let A be MSAlgebra-Family of I,S; ::_thesis: for s being SortSymbol of S
for U1 being non-empty MSAlgebra over S
for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st
( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds
for x being set st x in the Sorts of U1 . s holds
(commute ((commute F) . s)) . x in product (Carrier (A,s))
let s be SortSymbol of S; ::_thesis: for U1 being non-empty MSAlgebra over S
for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st
( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds
for x being set st x in the Sorts of U1 . s holds
(commute ((commute F) . s)) . x in product (Carrier (A,s))
let U1 be non-empty MSAlgebra over S; ::_thesis: for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st
( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds
for x being set st x in the Sorts of U1 . s holds
(commute ((commute F) . s)) . x in product (Carrier (A,s))
set SU = the Sorts of U1;
set SA = union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } ;
let F be ManySortedFunction of I; ::_thesis: ( ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st
( F1 = F . i & F1 is_homomorphism U1,A . i ) ) implies for x being set st x in the Sorts of U1 . s holds
(commute ((commute F) . s)) . x in product (Carrier (A,s)) )
assume A1: for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st
( F1 = F . i & F1 is_homomorphism U1,A . i ) ; ::_thesis: for x being set st x in the Sorts of U1 . s holds
(commute ((commute F) . s)) . x in product (Carrier (A,s))
(commute F) . s in Funcs (I,(Funcs (( the Sorts of U1 . s),(union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } )))) by A1, Th26;
then commute ((commute F) . s) in Funcs (( the Sorts of U1 . s),(Funcs (I,(union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } )))) by FUNCT_6:55;
then consider f9 being Function such that
A2: f9 = commute ((commute F) . s) and
A3: dom f9 = the Sorts of U1 . s and
A4: rng f9 c= Funcs (I,(union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } )) by FUNCT_2:def_2;
let x be set ; ::_thesis: ( x in the Sorts of U1 . s implies (commute ((commute F) . s)) . x in product (Carrier (A,s)) )
assume A5: x in the Sorts of U1 . s ; ::_thesis: (commute ((commute F) . s)) . x in product (Carrier (A,s))
f9 . x in rng f9 by A5, A3, FUNCT_1:def_3;
then consider f being Function such that
A6: f = (commute ((commute F) . s)) . x and
A7: dom f = I and
rng f c= union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } by A2, A4, FUNCT_2:def_2;
A8: now__::_thesis:_for_i1_being_set_st_i1_in_dom_(Carrier_(A,s))_holds_
((commute_((commute_F)_._s))_._x)_._i1_in_(Carrier_(A,s))_._i1
let i1 be set ; ::_thesis: ( i1 in dom (Carrier (A,s)) implies ((commute ((commute F) . s)) . x) . i1 in (Carrier (A,s)) . i1 )
assume i1 in dom (Carrier (A,s)) ; ::_thesis: ((commute ((commute F) . s)) . x) . i1 in (Carrier (A,s)) . i1
then reconsider i9 = i1 as Element of I ;
consider F1 being ManySortedFunction of U1,(A . i9) such that
A9: F1 = F . i9 and
F1 is_homomorphism U1,A . i9 by A1;
x in dom (F1 . s) by A5, FUNCT_2:def_1;
then A10: ( ex U0 being MSAlgebra over S st
( U0 = A . i9 & (Carrier (A,s)) . i9 = the Sorts of U0 . s ) & (F1 . s) . x in rng (F1 . s) ) by FUNCT_1:def_3, PRALG_2:def_9;
f . i9 = (F1 . s) . x by A1, A5, A6, A9, Th27;
hence ((commute ((commute F) . s)) . x) . i1 in (Carrier (A,s)) . i1 by A6, A10; ::_thesis: verum
end;
dom ((commute ((commute F) . s)) . x) = dom (Carrier (A,s)) by A6, A7, PARTFUN1:def_2;
hence (commute ((commute F) . s)) . x in product (Carrier (A,s)) by A8, CARD_3:9; ::_thesis: verum
end;
theorem :: PRALG_3:29
for I being non empty set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for U1 being non-empty MSAlgebra over S
for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st
( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds
ex H being ManySortedFunction of U1,(product A) st
( H is_homomorphism U1, product A & ( for i being Element of I holds (proj (A,i)) ** H = F . i ) )
proof
let I be non empty set ; ::_thesis: for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for U1 being non-empty MSAlgebra over S
for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st
( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds
ex H being ManySortedFunction of U1,(product A) st
( H is_homomorphism U1, product A & ( for i being Element of I holds (proj (A,i)) ** H = F . i ) )
let S be non empty non void ManySortedSign ; ::_thesis: for A being MSAlgebra-Family of I,S
for U1 being non-empty MSAlgebra over S
for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st
( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds
ex H being ManySortedFunction of U1,(product A) st
( H is_homomorphism U1, product A & ( for i being Element of I holds (proj (A,i)) ** H = F . i ) )
let A be MSAlgebra-Family of I,S; ::_thesis: for U1 being non-empty MSAlgebra over S
for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st
( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds
ex H being ManySortedFunction of U1,(product A) st
( H is_homomorphism U1, product A & ( for i being Element of I holds (proj (A,i)) ** H = F . i ) )
let U1 be non-empty MSAlgebra over S; ::_thesis: for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st
( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds
ex H being ManySortedFunction of U1,(product A) st
( H is_homomorphism U1, product A & ( for i being Element of I holds (proj (A,i)) ** H = F . i ) )
let F be ManySortedFunction of I; ::_thesis: ( ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st
( F1 = F . i & F1 is_homomorphism U1,A . i ) ) implies ex H being ManySortedFunction of U1,(product A) st
( H is_homomorphism U1, product A & ( for i being Element of I holds (proj (A,i)) ** H = F . i ) ) )
assume A1: for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st
( F1 = F . i & F1 is_homomorphism U1,A . i ) ; ::_thesis: ex H being ManySortedFunction of U1,(product A) st
( H is_homomorphism U1, product A & ( for i being Element of I holds (proj (A,i)) ** H = F . i ) )
set SU = the Sorts of U1;
set CA = the carrier of S;
set SA = union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } ;
deffunc H1( Element of S) -> set = commute ((commute F) . $1);
consider H being ManySortedSet of the carrier of S such that
A2: for s9 being Element of the carrier of S holds H . s9 = H1(s9) from PBOOLE:sch_5();
now__::_thesis:_for_s9_being_set_st_s9_in_the_carrier_of_S_holds_
H_._s9_is_Function_of_(_the_Sorts_of_U1_._s9),(_the_Sorts_of_(product_A)_._s9)
let s9 be set ; ::_thesis: ( s9 in the carrier of S implies H . s9 is Function of ( the Sorts of U1 . s9),( the Sorts of (product A) . s9) )
assume A3: s9 in the carrier of S ; ::_thesis: H . s9 is Function of ( the Sorts of U1 . s9),( the Sorts of (product A) . s9)
then reconsider s99 = s9 as SortSymbol of S ;
(commute F) . s9 in Funcs (I,(Funcs (( the Sorts of U1 . s9),(union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } )))) by A1, A3, Th26;
then commute ((commute F) . s9) in Funcs (( the Sorts of U1 . s9),(Funcs (I,(union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } )))) by A3, FUNCT_6:55;
then H . s9 in Funcs (( the Sorts of U1 . s9),(Funcs (I,(union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } )))) by A2, A3;
then consider Hs being Function such that
A4: Hs = H . s9 and
A5: dom Hs = the Sorts of U1 . s9 and
A6: rng Hs c= Funcs (I,(union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } )) by FUNCT_2:def_2;
rng Hs c= the Sorts of (product A) . s9
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng Hs or x in the Sorts of (product A) . s9 )
assume A7: x in rng Hs ; ::_thesis: x in the Sorts of (product A) . s9
then consider f being Function such that
A8: f = x and
A9: dom f = I and
rng f c= union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } by A6, FUNCT_2:def_2;
consider x1 being set such that
A10: x1 in dom Hs and
A11: Hs . x1 = f by A7, A8, FUNCT_1:def_3;
A12: now__::_thesis:_for_i9_being_set_st_i9_in_dom_(Carrier_(A,s99))_holds_
f_._i9_in_(Carrier_(A,s99))_._i9
let i9 be set ; ::_thesis: ( i9 in dom (Carrier (A,s99)) implies f . i9 in (Carrier (A,s99)) . i9 )
assume i9 in dom (Carrier (A,s99)) ; ::_thesis: f . i9 in (Carrier (A,s99)) . i9
then reconsider i99 = i9 as Element of I ;
consider F9 being ManySortedFunction of U1,(A . i99) such that
A13: F9 = F . i99 and
F9 is_homomorphism U1,A . i99 by A1;
H . s99 = commute ((commute F) . s99) by A2;
then A14: f . i99 = (F9 . s99) . x1 by A1, A4, A5, A10, A11, A13, Th27;
dom (F9 . s99) = dom Hs by A5, FUNCT_2:def_1;
then A15: (F9 . s9) . x1 in rng (F9 . s9) by A10, FUNCT_1:def_3;
( ex U0 being MSAlgebra over S st
( U0 = A . i99 & (Carrier (A,s99)) . i99 = the Sorts of U0 . s99 ) & rng (F9 . s99) c= the Sorts of (A . i99) . s99 ) by PRALG_2:def_9;
hence f . i9 in (Carrier (A,s99)) . i9 by A14, A15; ::_thesis: verum
end;
dom (Carrier (A,s99)) = dom f by A9, PARTFUN1:def_2;
then f in product (Carrier (A,s99)) by A12, CARD_3:9;
hence x in the Sorts of (product A) . s9 by A8, PRALG_2:def_10; ::_thesis: verum
end;
hence H . s9 is Function of ( the Sorts of U1 . s9),( the Sorts of (product A) . s9) by A3, A4, A5, FUNCT_2:def_1, RELSET_1:4; ::_thesis: verum
end;
then reconsider H = H as ManySortedFunction of U1,(product A) by PBOOLE:def_15;
A16: H is_homomorphism U1, product A
proof
let o be OperSymbol of S; :: according to MSUALG_3:def_7 ::_thesis: ( Args (o,U1) = {} or for b1 being Element of Args (o,U1) holds (H . (the_result_sort_of o)) . ((Den (o,U1)) . b1) = (Den (o,(product A))) . (H # b1) )
assume Args (o,U1) <> {} ; ::_thesis: for b1 being Element of Args (o,U1) holds (H . (the_result_sort_of o)) . ((Den (o,U1)) . b1) = (Den (o,(product A))) . (H # b1)
let x be Element of Args (o,U1); ::_thesis: (H . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,(product A))) . (H # x)
set s9 = the_result_sort_of o;
A17: Result (o,U1) = the Sorts of U1 . (the_result_sort_of o) by PRALG_2:3;
then A18: (Den (o,U1)) . x in the Sorts of U1 . (the_result_sort_of o) ;
thus (H . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,(product A))) . (H # x) ::_thesis: verum
proof
percases ( the_arity_of o = {} or the_arity_of o <> {} ) ;
supposeA19: the_arity_of o = {} ; ::_thesis: (H . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,(product A))) . (H # x)
set f = (commute ((commute F) . (the_result_sort_of o))) . (const (o,U1));
Args (o,U1) = {{}} by A19, PRALG_2:4;
then A20: x = {} by TARSKI:def_1;
A21: now__::_thesis:_for_i9_being_set_st_i9_in_I_holds_
((commute_((commute_F)_._(the_result_sort_of_o)))_._(const_(o,U1)))_._i9_=_(const_(o,(product_A)))_._i9
let i9 be set ; ::_thesis: ( i9 in I implies ((commute ((commute F) . (the_result_sort_of o))) . (const (o,U1))) . i9 = (const (o,(product A))) . i9 )
assume i9 in I ; ::_thesis: ((commute ((commute F) . (the_result_sort_of o))) . (const (o,U1))) . i9 = (const (o,(product A))) . i9
then reconsider ii = i9 as Element of I ;
consider F1 being ManySortedFunction of U1,(A . ii) such that
A22: F1 = F . ii and
A23: F1 is_homomorphism U1,A . ii by A1;
A24: F1 # x = {} by A19, A20, Th11;
thus ((commute ((commute F) . (the_result_sort_of o))) . (const (o,U1))) . i9 = (F1 . (the_result_sort_of o)) . ((Den (o,U1)) . x) by A1, A17, A20, A22, Th27
.= const (o,(A . ii)) by A23, A24, MSUALG_3:def_7
.= (const (o,(product A))) . i9 by A19, Th9 ; ::_thesis: verum
end;
const (o,(product A)) in Funcs (I,(union { (Result (o,(A . i1))) where i1 is Element of I : verum } )) by A19, Th8;
then A25: ex Co being Function st
( Co = const (o,(product A)) & dom Co = I & rng Co c= union { (Result (o,(A . i1))) where i1 is Element of I : verum } ) by FUNCT_2:def_2;
(commute ((commute F) . (the_result_sort_of o))) . (const (o,U1)) in product (Carrier (A,(the_result_sort_of o))) by A1, A18, A20, Th28;
then dom ((commute ((commute F) . (the_result_sort_of o))) . (const (o,U1))) = dom (Carrier (A,(the_result_sort_of o))) by CARD_3:9
.= I by PARTFUN1:def_2 ;
then A26: (commute ((commute F) . (the_result_sort_of o))) . (const (o,U1)) = const (o,(product A)) by A25, A21, FUNCT_1:2;
H # x = {} by A19, A20, Th11;
hence (H . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,(product A))) . (H # x) by A2, A20, A26; ::_thesis: verum
end;
supposeA27: the_arity_of o <> {} ; ::_thesis: (H . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,(product A))) . (H # x)
A28: Den (o,(product A)) = (OPS A) . o by MSUALG_1:def_6
.= IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o)))) by PRALG_2:def_13
.= Commute (Frege (A ?. o)) by A27, FUNCOP_1:def_8 ;
A29: now__::_thesis:_for_y_being_Element_of_Args_(o,(product_A))_holds_(Den_(o,(product_A)))_._y_in_rng_(Frege_(A_?._o))
let y be Element of Args (o,(product A)); ::_thesis: (Den (o,(product A))) . y in rng (Frege (A ?. o))
commute y in product (doms (A ?. o)) by A27, Th17;
then A30: commute y in dom (Frege (A ?. o)) by PARTFUN1:def_2;
y in dom (Commute (Frege (A ?. o))) by A27, Th18;
then (Den (o,(product A))) . y = (Frege (A ?. o)) . (commute y) by A28, PRALG_2:def_1;
hence (Den (o,(product A))) . y in rng (Frege (A ?. o)) by A30, FUNCT_1:def_3; ::_thesis: verum
end;
then reconsider f1 = (Den (o,(product A))) . (H # x) as Function by PRALG_2:8;
f1 in rng (Frege (A ?. o)) by A29;
then A31: dom f1 = I by PRALG_2:9;
set D = union { ( the Sorts of (A . i9) . ss) where i9 is Element of I, ss is Element of the carrier of S : verum } ;
set f = (commute ((commute F) . (the_result_sort_of o))) . ((Den (o,U1)) . x);
A32: H # x in Funcs ((dom (the_arity_of o)),(Funcs (I,(union { ( the Sorts of (A . i9) . ss) where i9 is Element of I, ss is Element of the carrier of S : verum } )))) by Th14;
A33: now__::_thesis:_for_i9_being_set_st_i9_in_I_holds_
((commute_((commute_F)_._(the_result_sort_of_o)))_._((Den_(o,U1))_._x))_._i9_=_f1_._i9
let i9 be set ; ::_thesis: ( i9 in I implies ((commute ((commute F) . (the_result_sort_of o))) . ((Den (o,U1)) . x)) . i9 = f1 . i9 )
assume i9 in I ; ::_thesis: ((commute ((commute F) . (the_result_sort_of o))) . ((Den (o,U1)) . x)) . i9 = f1 . i9
then reconsider ii = i9 as Element of I ;
consider F1 being ManySortedFunction of U1,(A . ii) such that
A34: F1 = F . ii and
A35: F1 is_homomorphism U1,A . ii by A1;
A36: (F1 . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,(A . ii))) . (F1 # x) by A35, MSUALG_3:def_7;
A37: now__::_thesis:_for_n_being_set_st_n_in_dom_(the_arity_of_o)_holds_
((commute_(H_#_x))_._ii)_._n_=_(F1_#_x)_._n
let n be set ; ::_thesis: ( n in dom (the_arity_of o) implies ((commute (H # x)) . ii) . n = (F1 # x) . n )
assume A38: n in dom (the_arity_of o) ; ::_thesis: ((commute (H # x)) . ii) . n = (F1 # x) . n
then (the_arity_of o) . n in rng (the_arity_of o) by FUNCT_1:def_3;
then reconsider s1 = (the_arity_of o) . n as Element of the carrier of S ;
A39: (F1 # x) . n = (F1 . ((the_arity_of o) /. n)) . (x . n) by A38, Th13
.= (F1 . s1) . (x . n) by A38, PARTFUN1:def_6 ;
x in Args (o,U1) ;
then A40: x in product ( the Sorts of U1 * (the_arity_of o)) by PRALG_2:3;
then A41: dom x = dom ( the Sorts of U1 * (the_arity_of o)) by CARD_3:9;
A42: dom x = dom ( the Sorts of U1 * (the_arity_of o)) by A40, CARD_3:9
.= dom (the_arity_of o) by PRALG_2:3 ;
then x . n in ( the Sorts of U1 * (the_arity_of o)) . n by A38, A40, A41, CARD_3:9;
then A43: x . n in the Sorts of U1 . s1 by A38, A42, A41, FUNCT_1:12;
A44: (H # x) . n = (H . ((the_arity_of o) /. n)) . (x . n) by A38, Th13
.= (H . s1) . (x . n) by A38, PARTFUN1:def_6
.= (commute ((commute F) . s1)) . (x . n) by A2 ;
then reconsider g = (H # x) . n as Function ;
thus ((commute (H # x)) . ii) . n = g . ii by A32, A38, FUNCT_6:56
.= (F1 # x) . n by A1, A34, A43, A39, A44, Th27 ; ::_thesis: verum
end;
dom F1 = the carrier of S by PARTFUN1:def_2;
then A45: rng (the_arity_of o) c= dom F1 ;
commute (H # x) in Funcs (I,(Funcs ((dom (the_arity_of o)),(union { ( the Sorts of (A . i9) . ss) where i9 is Element of I, ss is Element of the carrier of S : verum } )))) by A27, A32, FUNCT_6:55;
then consider ff being Function such that
A46: ff = commute (H # x) and
A47: dom ff = I and
A48: rng ff c= Funcs ((dom (the_arity_of o)),(union { ( the Sorts of (A . i9) . ss) where i9 is Element of I, ss is Element of the carrier of S : verum } )) by FUNCT_2:def_2;
ff . ii in rng ff by A47, FUNCT_1:def_3;
then A49: ex gg being Function st
( gg = (commute (H # x)) . ii & dom gg = dom (the_arity_of o) & rng gg c= union { ( the Sorts of (A . i9) . ss) where i9 is Element of I, ss is Element of the carrier of S : verum } ) by A46, A48, FUNCT_2:def_2;
A50: x in product (doms (F1 * (the_arity_of o))) by Th12;
dom (F1 # x) = dom ((Frege (F1 * (the_arity_of o))) . x) by MSUALG_3:def_5
.= dom ((F1 * (the_arity_of o)) .. x) by A50, PRALG_2:def_2
.= dom (F1 * (the_arity_of o)) by PRALG_1:def_17
.= dom (the_arity_of o) by A45, RELAT_1:27 ;
then F1 # x = (commute (H # x)) . ii by A49, A37, FUNCT_1:2;
then ((commute ((commute F) . (the_result_sort_of o))) . ((Den (o,U1)) . x)) . i9 = (Den (o,(A . ii))) . ((commute (H # x)) . ii) by A1, A17, A34, A36, Th27
.= f1 . i9 by A27, Th22 ;
hence ((commute ((commute F) . (the_result_sort_of o))) . ((Den (o,U1)) . x)) . i9 = f1 . i9 ; ::_thesis: verum
end;
(commute ((commute F) . (the_result_sort_of o))) . ((Den (o,U1)) . x) in product (Carrier (A,(the_result_sort_of o))) by A1, A17, Th28;
then dom ((commute ((commute F) . (the_result_sort_of o))) . ((Den (o,U1)) . x)) = dom (Carrier (A,(the_result_sort_of o))) by CARD_3:9
.= I by PARTFUN1:def_2 ;
then (commute ((commute F) . (the_result_sort_of o))) . ((Den (o,U1)) . x) = f1 by A31, A33, FUNCT_1:2;
hence (H . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,(product A))) . (H # x) by A2; ::_thesis: verum
end;
end;
end;
end;
take H ; ::_thesis: ( H is_homomorphism U1, product A & ( for i being Element of I holds (proj (A,i)) ** H = F . i ) )
for i being Element of I holds (proj (A,i)) ** H = F . i
proof
let i be Element of I; ::_thesis: (proj (A,i)) ** H = F . i
consider F1 being ManySortedFunction of U1,(A . i) such that
A51: F1 = F . i and
F1 is_homomorphism U1,A . i by A1;
A52: dom ((proj (A,i)) ** H) = (dom (proj (A,i))) /\ (dom H) by PBOOLE:def_19
.= the carrier of S /\ (dom H) by PARTFUN1:def_2
.= the carrier of S /\ the carrier of S by PARTFUN1:def_2
.= the carrier of S ;
A53: now__::_thesis:_for_s9_being_set_st_s9_in_the_carrier_of_S_holds_
((proj_(A,i))_**_H)_._s9_=_F1_._s9
let s9 be set ; ::_thesis: ( s9 in the carrier of S implies ((proj (A,i)) ** H) . s9 = F1 . s9 )
assume s9 in the carrier of S ; ::_thesis: ((proj (A,i)) ** H) . s9 = F1 . s9
then reconsider s1 = s9 as SortSymbol of S ;
A54: ((proj (A,i)) ** H) . s9 = ((proj (A,i)) . s1) * (H . s1) by A52, PBOOLE:def_19
.= (proj ((Carrier (A,s1)),i)) * (H . s1) by Def2
.= (proj ((Carrier (A,s1)),i)) * (commute ((commute F) . s1)) by A2 ;
(commute F) . s1 in Funcs (I,(Funcs (( the Sorts of U1 . s1),(union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } )))) by A1, Th26;
then commute ((commute F) . s1) in Funcs (( the Sorts of U1 . s1),(Funcs (I,(union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } )))) by FUNCT_6:55;
then consider f9 being Function such that
A55: f9 = commute ((commute F) . s1) and
A56: dom f9 = the Sorts of U1 . s1 and
rng f9 c= Funcs (I,(union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } )) by FUNCT_2:def_2;
rng f9 c= dom (proj ((Carrier (A,s1)),i))
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f9 or y in dom (proj ((Carrier (A,s1)),i)) )
assume y in rng f9 ; ::_thesis: y in dom (proj ((Carrier (A,s1)),i))
then consider x9 being set such that
A57: x9 in dom f9 and
A58: f9 . x9 = y by FUNCT_1:def_3;
(commute ((commute F) . s1)) . x9 in product (Carrier (A,s1)) by A1, A56, A57, Th28;
hence y in dom (proj ((Carrier (A,s1)),i)) by A55, A58, CARD_3:def_16; ::_thesis: verum
end;
then A59: dom (((proj (A,i)) ** H) . s9) = the Sorts of U1 . s9 by A55, A56, A54, RELAT_1:27;
A60: now__::_thesis:_for_x_being_set_st_x_in_the_Sorts_of_U1_._s9_holds_
(((proj_(A,i))_**_H)_._s9)_._x_=_(F1_._s9)_._x
let x be set ; ::_thesis: ( x in the Sorts of U1 . s9 implies (((proj (A,i)) ** H) . s9) . x = (F1 . s9) . x )
assume A61: x in the Sorts of U1 . s9 ; ::_thesis: (((proj (A,i)) ** H) . s9) . x = (F1 . s9) . x
then (commute ((commute F) . s1)) . x in product (Carrier (A,s1)) by A1, Th28;
then A62: (commute ((commute F) . s1)) . x in dom (proj ((Carrier (A,s1)),i)) by CARD_3:def_16;
thus (((proj (A,i)) ** H) . s9) . x = (proj ((Carrier (A,s1)),i)) . ((commute ((commute F) . s1)) . x) by A54, A59, A61, FUNCT_1:12
.= ((commute ((commute F) . s1)) . x) . i by A62, CARD_3:def_16
.= (F1 . s9) . x by A1, A51, A61, Th27 ; ::_thesis: verum
end;
dom (F1 . s9) = dom (F1 . s1)
.= the Sorts of U1 . s9 by FUNCT_2:def_1 ;
hence ((proj (A,i)) ** H) . s9 = F1 . s9 by A59, A60, FUNCT_1:2; ::_thesis: verum
end;
dom F1 = the carrier of S by PARTFUN1:def_2;
hence (proj (A,i)) ** H = F . i by A51, A52, A53, FUNCT_1:2; ::_thesis: verum
end;
hence ( H is_homomorphism U1, product A & ( for i being Element of I holds (proj (A,i)) ** H = F . i ) ) by A16; ::_thesis: verum
end;
begin
definition
let I be non empty set ;
let J be ManySortedSet of I;
let S be non empty non void ManySortedSign ;
mode MSAlgebra-Class of S,J -> ManySortedSet of I means :Def3: :: PRALG_3:def 3
for i being set st i in I holds
it . i is MSAlgebra-Family of J . i,S;
existence
ex b1 being ManySortedSet of I st
for i being set st i in I holds
b1 . i is MSAlgebra-Family of J . i,S
proof
defpred S1[ set , set ] means $2 is MSAlgebra-Family of J . $1,S;
A1: for i being set st i in I holds
ex F being set st S1[i,F]
proof
let i be set ; ::_thesis: ( i in I implies ex F being set st S1[i,F] )
assume i in I ; ::_thesis: ex F being set st S1[i,F]
set F = the MSAlgebra-Family of J . i,S;
take the MSAlgebra-Family of J . i,S ; ::_thesis: S1[i, the MSAlgebra-Family of J . i,S]
thus S1[i, the MSAlgebra-Family of J . i,S] ; ::_thesis: verum
end;
consider C being ManySortedSet of I such that
A2: for i being set st i in I holds
S1[i,C . i] from PBOOLE:sch_3(A1);
take C ; ::_thesis: for i being set st i in I holds
C . i is MSAlgebra-Family of J . i,S
thus for i being set st i in I holds
C . i is MSAlgebra-Family of J . i,S by A2; ::_thesis: verum
end;
end;
:: deftheorem Def3 defines MSAlgebra-Class PRALG_3:def_3_:_
for I being non empty set
for J being ManySortedSet of I
for S being non empty non void ManySortedSign
for b4 being ManySortedSet of I holds
( b4 is MSAlgebra-Class of S,J iff for i being set st i in I holds
b4 . i is MSAlgebra-Family of J . i,S );
definition
let I be non empty set ;
let S be non empty non void ManySortedSign ;
let A be MSAlgebra-Family of I,S;
let EqR be Equivalence_Relation of I;
funcA / EqR -> MSAlgebra-Class of S, id (Class EqR) means :Def4: :: PRALG_3:def 4
for c being set st c in Class EqR holds
it . c = A | c;
existence
ex b1 being MSAlgebra-Class of S, id (Class EqR) st
for c being set st c in Class EqR holds
b1 . c = A | c
proof
thus ex X being MSAlgebra-Class of S, id (Class EqR) st
for c being set st c in Class EqR holds
X . c = A | c ::_thesis: verum
proof
deffunc H1( set ) -> set = A | $1;
consider X being ManySortedSet of Class EqR such that
A1: for c being set st c in Class EqR holds
X . c = H1(c) from PBOOLE:sch_4();
X is MSAlgebra-Class of S, id (Class EqR)
proof
let c be set ; :: according to PRALG_3:def_3 ::_thesis: ( c in Class EqR implies X . c is MSAlgebra-Family of (id (Class EqR)) . c,S )
assume A2: c in Class EqR ; ::_thesis: X . c is MSAlgebra-Family of (id (Class EqR)) . c,S
A3: dom (A | c) = (dom A) /\ c by RELAT_1:61
.= I /\ c by PARTFUN1:def_2
.= c by A2, XBOOLE_1:28
.= (id (Class EqR)) . c by A2, FUNCT_1:18 ;
then reconsider ac = A | c as ManySortedSet of (id (Class EqR)) . c by PARTFUN1:def_2, RELAT_1:def_18;
ac is MSAlgebra-Family of (id (Class EqR)) . c,S
proof
let i be set ; :: according to PRALG_2:def_5 ::_thesis: ( not i in (id (Class EqR)) . c or ac . i is MSAlgebra over S )
assume A4: i in (id (Class EqR)) . c ; ::_thesis: ac . i is MSAlgebra over S
dom ac = c by A2, A3, FUNCT_1:18;
then reconsider i9 = i as Element of I by A2, A3, A4;
A . i9 is non-empty MSAlgebra over S ;
hence ac . i is MSAlgebra over S by A3, A4, FUNCT_1:47; ::_thesis: verum
end;
hence X . c is MSAlgebra-Family of (id (Class EqR)) . c,S by A1, A2; ::_thesis: verum
end;
then reconsider X = X as MSAlgebra-Class of S, id (Class EqR) ;
take X ; ::_thesis: for c being set st c in Class EqR holds
X . c = A | c
thus for c being set st c in Class EqR holds
X . c = A | c by A1; ::_thesis: verum
end;
end;
uniqueness
for b1, b2 being MSAlgebra-Class of S, id (Class EqR) st ( for c being set st c in Class EqR holds
b1 . c = A | c ) & ( for c being set st c in Class EqR holds
b2 . c = A | c ) holds
b1 = b2
proof
for X, Y being MSAlgebra-Class of S, id (Class EqR) st ( for c being set st c in Class EqR holds
X . c = A | c ) & ( for c being set st c in Class EqR holds
Y . c = A | c ) holds
X = Y
proof
let X, Y be MSAlgebra-Class of S, id (Class EqR); ::_thesis: ( ( for c being set st c in Class EqR holds
X . c = A | c ) & ( for c being set st c in Class EqR holds
Y . c = A | c ) implies X = Y )
assume that
A5: for c being set st c in Class EqR holds
X . c = A | c and
A6: for c being set st c in Class EqR holds
Y . c = A | c ; ::_thesis: X = Y
now__::_thesis:_for_c_being_set_st_c_in_Class_EqR_holds_
X_._c_=_Y_._c
let c be set ; ::_thesis: ( c in Class EqR implies X . c = Y . c )
assume A7: c in Class EqR ; ::_thesis: X . c = Y . c
hence X . c = A | c by A5
.= Y . c by A6, A7 ;
::_thesis: verum
end;
hence X = Y by PBOOLE:3; ::_thesis: verum
end;
hence for b1, b2 being MSAlgebra-Class of S, id (Class EqR) st ( for c being set st c in Class EqR holds
b1 . c = A | c ) & ( for c being set st c in Class EqR holds
b2 . c = A | c ) holds
b1 = b2 ; ::_thesis: verum
end;
end;
:: deftheorem Def4 defines / PRALG_3:def_4_:_
for I being non empty set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for EqR being Equivalence_Relation of I
for b5 being MSAlgebra-Class of S, id (Class EqR) holds
( b5 = A / EqR iff for c being set st c in Class EqR holds
b5 . c = A | c );
definition
let I be non empty set ;
let S be non empty non void ManySortedSign ;
let J be V8() ManySortedSet of I;
let C be MSAlgebra-Class of S,J;
func product C -> MSAlgebra-Family of I,S means :Def5: :: PRALG_3:def 5
for i being Element of I st i in I holds
ex Ji being non empty set ex Cs being MSAlgebra-Family of Ji,S st
( Ji = J . i & Cs = C . i & it . i = product Cs );
existence
ex b1 being MSAlgebra-Family of I,S st
for i being Element of I st i in I holds
ex Ji being non empty set ex Cs being MSAlgebra-Family of Ji,S st
( Ji = J . i & Cs = C . i & b1 . i = product Cs )
proof
thus ex PC being MSAlgebra-Family of I,S st
for i being Element of I st i in I holds
ex Ji being non empty set ex Cs being MSAlgebra-Family of Ji,S st
( Ji = J . i & Cs = C . i & PC . i = product Cs ) ::_thesis: verum
proof
defpred S1[ set , set ] means ex Ji being non empty set ex Cs being MSAlgebra-Family of Ji,S st
( Ji = J . $1 & Cs = C . $1 & $2 = product Cs );
A1: now__::_thesis:_for_i_being_set_st_i_in_I_holds_
ex_j_being_set_st_S1[i,j]
let i be set ; ::_thesis: ( i in I implies ex j being set st S1[i,j] )
assume A2: i in I ; ::_thesis: ex j being set st S1[i,j]
then reconsider Ji = J . i as non empty set ;
reconsider Cs = C . i as MSAlgebra-Family of Ji,S by A2, Def3;
ex a being set st a = product Cs ;
then consider j being set such that
A3: ex Ji being non empty set ex Cs being MSAlgebra-Family of Ji,S st
( Ji = J . i & Cs = C . i & j = product Cs ) ;
take j = j; ::_thesis: S1[i,j]
thus S1[i,j] by A3; ::_thesis: verum
end;
consider PC being ManySortedSet of I such that
A4: for i being set st i in I holds
S1[i,PC . i] from PBOOLE:sch_3(A1);
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
PC_._i_is_non-empty_MSAlgebra_over_S
let i be set ; ::_thesis: ( i in I implies PC . i is non-empty MSAlgebra over S )
assume i in I ; ::_thesis: PC . i is non-empty MSAlgebra over S
then ex Ji being non empty set ex Cs being MSAlgebra-Family of Ji,S st
( Ji = J . i & Cs = C . i & PC . i = product Cs ) by A4;
hence PC . i is non-empty MSAlgebra over S ; ::_thesis: verum
end;
then reconsider PC = PC as MSAlgebra-Family of I,S by PRALG_2:def_5;
take PC ; ::_thesis: for i being Element of I st i in I holds
ex Ji being non empty set ex Cs being MSAlgebra-Family of Ji,S st
( Ji = J . i & Cs = C . i & PC . i = product Cs )
thus for i being Element of I st i in I holds
ex Ji being non empty set ex Cs being MSAlgebra-Family of Ji,S st
( Ji = J . i & Cs = C . i & PC . i = product Cs ) by A4; ::_thesis: verum
end;
end;
uniqueness
for b1, b2 being MSAlgebra-Family of I,S st ( for i being Element of I st i in I holds
ex Ji being non empty set ex Cs being MSAlgebra-Family of Ji,S st
( Ji = J . i & Cs = C . i & b1 . i = product Cs ) ) & ( for i being Element of I st i in I holds
ex Ji being non empty set ex Cs being MSAlgebra-Family of Ji,S st
( Ji = J . i & Cs = C . i & b2 . i = product Cs ) ) holds
b1 = b2
proof
for PC1, PC2 being MSAlgebra-Family of I,S st ( for i being Element of I st i in I holds
ex Ji being non empty set ex Cs being MSAlgebra-Family of Ji,S st
( Ji = J . i & Cs = C . i & PC1 . i = product Cs ) ) & ( for i being Element of I st i in I holds
ex Ji being non empty set ex Cs being MSAlgebra-Family of Ji,S st
( Ji = J . i & Cs = C . i & PC2 . i = product Cs ) ) holds
PC1 = PC2
proof
let PC1, PC2 be MSAlgebra-Family of I,S; ::_thesis: ( ( for i being Element of I st i in I holds
ex Ji being non empty set ex Cs being MSAlgebra-Family of Ji,S st
( Ji = J . i & Cs = C . i & PC1 . i = product Cs ) ) & ( for i being Element of I st i in I holds
ex Ji being non empty set ex Cs being MSAlgebra-Family of Ji,S st
( Ji = J . i & Cs = C . i & PC2 . i = product Cs ) ) implies PC1 = PC2 )
assume A5: ( ( for i being Element of I st i in I holds
ex Ji being non empty set ex Cs being MSAlgebra-Family of Ji,S st
( Ji = J . i & Cs = C . i & PC1 . i = product Cs ) ) & ( for i being Element of I st i in I holds
ex Ji being non empty set ex Cs being MSAlgebra-Family of Ji,S st
( Ji = J . i & Cs = C . i & PC2 . i = product Cs ) ) ) ; ::_thesis: PC1 = PC2
now__::_thesis:_for_i1_being_set_st_i1_in_I_holds_
PC1_._i1_=_PC2_._i1
let i1 be set ; ::_thesis: ( i1 in I implies PC1 . i1 = PC2 . i1 )
assume i1 in I ; ::_thesis: PC1 . i1 = PC2 . i1
then reconsider i9 = i1 as Element of I ;
( ex Ji1 being non empty set ex Cs1 being MSAlgebra-Family of Ji1,S st
( Ji1 = J . i9 & Cs1 = C . i9 & PC1 . i9 = product Cs1 ) & ex Ji2 being non empty set ex Cs2 being MSAlgebra-Family of Ji2,S st
( Ji2 = J . i9 & Cs2 = C . i9 & PC2 . i9 = product Cs2 ) ) by A5;
hence PC1 . i1 = PC2 . i1 ; ::_thesis: verum
end;
hence PC1 = PC2 by PBOOLE:3; ::_thesis: verum
end;
hence for b1, b2 being MSAlgebra-Family of I,S st ( for i being Element of I st i in I holds
ex Ji being non empty set ex Cs being MSAlgebra-Family of Ji,S st
( Ji = J . i & Cs = C . i & b1 . i = product Cs ) ) & ( for i being Element of I st i in I holds
ex Ji being non empty set ex Cs being MSAlgebra-Family of Ji,S st
( Ji = J . i & Cs = C . i & b2 . i = product Cs ) ) holds
b1 = b2 ; ::_thesis: verum
end;
end;
:: deftheorem Def5 defines product PRALG_3:def_5_:_
for I being non empty set
for S being non empty non void ManySortedSign
for J being V8() ManySortedSet of I
for C being MSAlgebra-Class of S,J
for b5 being MSAlgebra-Family of I,S holds
( b5 = product C iff for i being Element of I st i in I holds
ex Ji being non empty set ex Cs being MSAlgebra-Family of Ji,S st
( Ji = J . i & Cs = C . i & b5 . i = product Cs ) );
theorem :: PRALG_3:30
for I being non empty set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for EqR being Equivalence_Relation of I holds product A, product (product (A / EqR)) are_isomorphic
proof
let I be non empty set ; ::_thesis: for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for EqR being Equivalence_Relation of I holds product A, product (product (A / EqR)) are_isomorphic
let S be non empty non void ManySortedSign ; ::_thesis: for A being MSAlgebra-Family of I,S
for EqR being Equivalence_Relation of I holds product A, product (product (A / EqR)) are_isomorphic
let A be MSAlgebra-Family of I,S; ::_thesis: for EqR being Equivalence_Relation of I holds product A, product (product (A / EqR)) are_isomorphic
let EqR be Equivalence_Relation of I; ::_thesis: product A, product (product (A / EqR)) are_isomorphic
set U1 = product A;
set U2 = product (product (A / EqR));
set U19 = the Sorts of (product A);
set U29 = the Sorts of (product (product (A / EqR)));
defpred S1[ set , set , set ] means for f1, g1 being Function st f1 = $2 & g1 = $1 holds
for e being Element of Class EqR holds g1 . e = f1 | e;
A1: for s being set st s in the carrier of S holds
for x being set st x in the Sorts of (product A) . s holds
ex y being set st
( y in the Sorts of (product (product (A / EqR))) . s & S1[y,x,s] )
proof
let s be set ; ::_thesis: ( s in the carrier of S implies for x being set st x in the Sorts of (product A) . s holds
ex y being set st
( y in the Sorts of (product (product (A / EqR))) . s & S1[y,x,s] ) )
assume s in the carrier of S ; ::_thesis: for x being set st x in the Sorts of (product A) . s holds
ex y being set st
( y in the Sorts of (product (product (A / EqR))) . s & S1[y,x,s] )
then reconsider s9 = s as SortSymbol of S ;
A2: the Sorts of (product A) . s9 = product (Carrier (A,s9)) by PRALG_2:def_10;
let x be set ; ::_thesis: ( x in the Sorts of (product A) . s implies ex y being set st
( y in the Sorts of (product (product (A / EqR))) . s & S1[y,x,s] ) )
assume A3: x in the Sorts of (product A) . s ; ::_thesis: ex y being set st
( y in the Sorts of (product (product (A / EqR))) . s & S1[y,x,s] )
reconsider x = x as Function by A3, A2;
deffunc H1( set ) -> set = x | $1;
consider y being ManySortedSet of Class EqR such that
A4: for c being set st c in Class EqR holds
y . c = H1(c) from PBOOLE:sch_4();
A5: dom (Carrier ((product (A / EqR)),s9)) = Class EqR by PARTFUN1:def_2;
A6: for a being set st a in dom (Carrier ((product (A / EqR)),s9)) holds
y . a in (Carrier ((product (A / EqR)),s9)) . a
proof
set A9 = product (A / EqR);
let a be set ; ::_thesis: ( a in dom (Carrier ((product (A / EqR)),s9)) implies y . a in (Carrier ((product (A / EqR)),s9)) . a )
assume A7: a in dom (Carrier ((product (A / EqR)),s9)) ; ::_thesis: y . a in (Carrier ((product (A / EqR)),s9)) . a
A8: (A / EqR) . a = A | a by A7, Def4;
reconsider a = a as non empty Subset of I by A5, A7;
A9: ex U0 being MSAlgebra over S st
( U0 = (product (A / EqR)) . a & (Carrier ((product (A / EqR)),s9)) . a = the Sorts of U0 . s9 ) by A7, PRALG_2:def_9;
A10: dom (A | a) = (dom A) /\ a by RELAT_1:61
.= I /\ a by PARTFUN1:def_2
.= a by XBOOLE_1:28 ;
then reconsider Aa1 = A | a as ManySortedSet of a by PARTFUN1:def_2;
for i being set st i in a holds
Aa1 . i is non-empty MSAlgebra over S
proof
let i be set ; ::_thesis: ( i in a implies Aa1 . i is non-empty MSAlgebra over S )
assume A11: i in a ; ::_thesis: Aa1 . i is non-empty MSAlgebra over S
then A . i is non-empty MSAlgebra over S by PRALG_2:def_5;
hence Aa1 . i is non-empty MSAlgebra over S by A10, A11, FUNCT_1:47; ::_thesis: verum
end;
then reconsider Aa = Aa1 as MSAlgebra-Family of a,S by PRALG_2:def_5;
x | a in product ((Carrier (A,s9)) | a) by A3, A2, Th1;
then A12: x | a in product (Carrier (Aa,s9)) by Th2;
consider Ji being non empty set , Cs being MSAlgebra-Family of Ji,S such that
A13: Ji = (id (Class EqR)) . a and
A14: ( Cs = (A / EqR) . a & (product (A / EqR)) . a = product Cs ) by A7, Def5;
Ji = a by A7, A13, FUNCT_1:18;
then (Carrier ((product (A / EqR)),s9)) . a = product (Carrier (Aa,s9)) by A8, A14, A9, PRALG_2:def_10;
hence y . a in (Carrier ((product (A / EqR)),s9)) . a by A4, A7, A12; ::_thesis: verum
end;
take y ; ::_thesis: ( y in the Sorts of (product (product (A / EqR))) . s & S1[y,x,s] )
dom (Carrier ((product (A / EqR)),s9)) = Class EqR by PARTFUN1:def_2
.= dom y by PARTFUN1:def_2 ;
then y in product (Carrier ((product (A / EqR)),s9)) by A6, CARD_3:9;
hence ( y in the Sorts of (product (product (A / EqR))) . s & S1[y,x,s] ) by A4, PRALG_2:def_10; ::_thesis: verum
end;
consider F being ManySortedFunction of the Sorts of (product A), the Sorts of (product (product (A / EqR))) such that
A15: for s being set st s in the carrier of S holds
ex f being Function of ( the Sorts of (product A) . s),( the Sorts of (product (product (A / EqR))) . s) st
( f = F . s & ( for x being set st x in the Sorts of (product A) . s holds
S1[f . x,x,s] ) ) from MSSUBFAM:sch_1(A1);
A16: F is_homomorphism product A, product (product (A / EqR))
proof
let o be OperSymbol of S; :: according to MSUALG_3:def_7 ::_thesis: ( Args (o,(product A)) = {} or for b1 being Element of Args (o,(product A)) holds (F . (the_result_sort_of o)) . ((Den (o,(product A))) . b1) = (Den (o,(product (product (A / EqR))))) . (F # b1) )
assume Args (o,(product A)) <> {} ; ::_thesis: for b1 being Element of Args (o,(product A)) holds (F . (the_result_sort_of o)) . ((Den (o,(product A))) . b1) = (Den (o,(product (product (A / EqR))))) . (F # b1)
let x be Element of Args (o,(product A)); ::_thesis: (F . (the_result_sort_of o)) . ((Den (o,(product A))) . x) = (Den (o,(product (product (A / EqR))))) . (F # x)
thus (F . (the_result_sort_of o)) . ((Den (o,(product A))) . x) = (Den (o,(product (product (A / EqR))))) . (F # x) ::_thesis: verum
proof
A17: (Den (o,(product A))) . x in Result (o,(product A)) ;
then A18: (Den (o,(product A))) . x in the Sorts of (product A) . (the_result_sort_of o) by PRALG_2:3;
set s = the_result_sort_of o;
set U3 = product (A / EqR);
A19: the Sorts of (product (product (A / EqR))) . (the_result_sort_of o) = product (Carrier ((product (A / EqR)),(the_result_sort_of o))) by PRALG_2:def_10;
A20: ex f being Function of ( the Sorts of (product A) . (the_result_sort_of o)),( the Sorts of (product (product (A / EqR))) . (the_result_sort_of o)) st
( f = F . (the_result_sort_of o) & ( for x9 being set st x9 in the Sorts of (product A) . (the_result_sort_of o) holds
S1[f . x9,x9, the_result_sort_of o] ) ) by A15;
A21: dom (F . (the_result_sort_of o)) = (SORTS A) . (the_result_sort_of o) by FUNCT_2:def_1
.= product (Carrier (A,(the_result_sort_of o))) by PRALG_2:def_10 ;
A22: (Den (o,(product A))) . x in product (Carrier (A,(the_result_sort_of o))) by Th19;
percases ( the_arity_of o = {} or the_arity_of o <> {} ) ;
supposeA23: the_arity_of o = {} ; ::_thesis: (F . (the_result_sort_of o)) . ((Den (o,(product A))) . x) = (Den (o,(product (product (A / EqR))))) . (F # x)
then Args (o,(product A)) = {{}} by PRALG_2:4;
then A24: x = {} by TARSKI:def_1;
then A25: (F . (the_result_sort_of o)) . (const (o,(product A))) in rng (F . (the_result_sort_of o)) by A21, A22, FUNCT_1:def_3;
reconsider g1 = (F . (the_result_sort_of o)) . (const (o,(product A))) as Function by A19;
A26: dom (const (o,(product A))) = dom (Carrier (A,(the_result_sort_of o))) by A22, A24, CARD_3:9
.= I by PARTFUN1:def_2 ;
A27: now__::_thesis:_for_e_being_Element_of_Class_EqR_holds_(const_(o,(product_A)))_|_e_=_const_(o,((product_(A_/_EqR))_._e))
let e be Element of Class EqR; ::_thesis: (const (o,(product A))) | e = const (o,((product (A / EqR)) . e))
consider Ji being non empty set , Cs being MSAlgebra-Family of Ji,S such that
A28: Ji = (id (Class EqR)) . e and
A29: Cs = (A / EqR) . e and
A30: (product (A / EqR)) . e = product Cs by Def5;
A31: dom ((const (o,(product A))) | e) = I /\ e by A26, RELAT_1:61
.= e by XBOOLE_1:28 ;
A32: now__::_thesis:_for_i1_being_set_st_i1_in_e_holds_
((const_(o,(product_A)))_|_e)_._i1_=_(const_(o,(product_Cs)))_._i1
let i1 be set ; ::_thesis: ( i1 in e implies ((const (o,(product A))) | e) . i1 = (const (o,(product Cs))) . i1 )
A33: dom (A | e) = (dom A) /\ e by RELAT_1:61
.= I /\ e by PARTFUN1:def_2
.= e by XBOOLE_1:28 ;
assume A34: i1 in e ; ::_thesis: ((const (o,(product A))) | e) . i1 = (const (o,(product Cs))) . i1
then reconsider ii = i1 as Element of Ji by A28, FUNCT_1:18;
reconsider ii9 = ii as Element of I by A34;
Cs = A | e by A29, Def4;
then A35: Cs . ii = A . ii9 by A34, A33, FUNCT_1:47;
thus ((const (o,(product A))) | e) . i1 = (const (o,(product A))) . i1 by A31, A34, FUNCT_1:47
.= const (o,(A . ii9)) by A23, Th9
.= (const (o,(product Cs))) . i1 by A23, A35, Th9 ; ::_thesis: verum
end;
const (o,(product Cs)) in Funcs (Ji,(union { (Result (o,(Cs . i9))) where i9 is Element of Ji : verum } )) by A23, Th8;
then dom (const (o,(product Cs))) = Ji by FUNCT_2:92
.= e by A28, FUNCT_1:18 ;
hence (const (o,(product A))) | e = const (o,((product (A / EqR)) . e)) by A30, A31, A32, FUNCT_1:2; ::_thesis: verum
end;
A36: const (o,(product A)) in the Sorts of (product A) . (the_result_sort_of o) by A17, A24, PRALG_2:3;
A37: now__::_thesis:_for_x1_being_set_st_x1_in_Class_EqR_holds_
g1_._x1_=_(const_(o,(product_(product_(A_/_EqR)))))_._x1
let x1 be set ; ::_thesis: ( x1 in Class EqR implies g1 . x1 = (const (o,(product (product (A / EqR))))) . x1 )
consider f1 being Function such that
A38: f1 = const (o,(product A)) ;
assume x1 in Class EqR ; ::_thesis: g1 . x1 = (const (o,(product (product (A / EqR))))) . x1
then reconsider e = x1 as Element of Class EqR ;
g1 . e = f1 | e by A20, A36, A38;
hence g1 . x1 = const (o,((product (A / EqR)) . e)) by A27, A38
.= (const (o,(product (product (A / EqR))))) . x1 by A23, Th9 ;
::_thesis: verum
end;
const (o,(product (product (A / EqR)))) in Funcs ((Class EqR),(union { (Result (o,((product (A / EqR)) . i9))) where i9 is Element of Class EqR : verum } )) by A23, Th8;
then A39: dom (const (o,(product (product (A / EqR))))) = Class EqR by FUNCT_2:92;
dom g1 = dom (Carrier ((product (A / EqR)),(the_result_sort_of o))) by A19, A25, CARD_3:9
.= Class EqR by PARTFUN1:def_2 ;
then (F . (the_result_sort_of o)) . (const (o,(product A))) = const (o,(product (product (A / EqR)))) by A39, A37, FUNCT_1:2;
hence (F . (the_result_sort_of o)) . ((Den (o,(product A))) . x) = (Den (o,(product (product (A / EqR))))) . (F # x) by A23, A24, Th11; ::_thesis: verum
end;
supposeA40: the_arity_of o <> {} ; ::_thesis: (F . (the_result_sort_of o)) . ((Den (o,(product A))) . x) = (Den (o,(product (product (A / EqR))))) . (F # x)
A41: (Den (o,(product (product (A / EqR))))) . (F # x) in product (Carrier ((product (A / EqR)),(the_result_sort_of o))) by Th19;
then reconsider f1 = (Den (o,(product (product (A / EqR))))) . (F # x) as Function ;
A42: dom f1 = dom (Carrier ((product (A / EqR)),(the_result_sort_of o))) by A41, CARD_3:9
.= Class EqR by PARTFUN1:def_2 ;
A43: (F . (the_result_sort_of o)) . ((Den (o,(product A))) . x) in rng (F . (the_result_sort_of o)) by A21, A22, FUNCT_1:def_3;
reconsider g1 = (F . (the_result_sort_of o)) . ((Den (o,(product A))) . x) as Function by A19;
A44: now__::_thesis:_for_e_being_Element_of_Class_EqR
for_f2_being_Function_st_f2_=_(Den_(o,(product_A)))_._x_holds_
f2_|_e_=_(Den_(o,((product_(A_/_EqR))_._e)))_._((commute_(F_#_x))_._e)
let e be Element of Class EqR; ::_thesis: for f2 being Function st f2 = (Den (o,(product A))) . x holds
f2 | e = (Den (o,((product (A / EqR)) . e))) . ((commute (F # x)) . e)
consider Ji being non empty set , Cs being MSAlgebra-Family of Ji,S such that
A45: Ji = (id (Class EqR)) . e and
A46: Cs = (A / EqR) . e and
A47: (product (A / EqR)) . e = product Cs by Def5;
A48: (commute (F # x)) . e is Element of Args (o,((product (A / EqR)) . e)) by A40, Th20;
then A49: (Den (o,((product (A / EqR)) . e))) . ((commute (F # x)) . e) in product (Carrier (Cs,(the_result_sort_of o))) by A47, Th19;
then reconsider f3 = (Den (o,((product (A / EqR)) . e))) . ((commute (F # x)) . e) as Function ;
A50: now__::_thesis:_for_i1_being_Element_of_I_st_i1_in_e_holds_
(commute_((commute_(F_#_x))_._e))_._i1_=_(commute_x)_._i1
let i1 be Element of I; ::_thesis: ( i1 in e implies (commute ((commute (F # x)) . e)) . i1 = (commute x) . i1 )
assume A51: i1 in e ; ::_thesis: (commute ((commute (F # x)) . e)) . i1 = (commute x) . i1
then reconsider i2 = i1 as Element of Ji by A45, FUNCT_1:18;
A52: now__::_thesis:_for_n_being_set_st_n_in_dom_(the_arity_of_o)_holds_
((commute_((commute_(F_#_x))_._e))_._i1)_._n_=_((commute_x)_._i1)_._n
let n be set ; ::_thesis: ( n in dom (the_arity_of o) implies ((commute ((commute (F # x)) . e)) . i1) . n = ((commute x) . i1) . n )
assume A53: n in dom (the_arity_of o) ; ::_thesis: ((commute ((commute (F # x)) . e)) . i1) . n = ((commute x) . i1) . n
then (the_arity_of o) . n in rng (the_arity_of o) by FUNCT_1:def_3;
then reconsider s1 = (the_arity_of o) . n as SortSymbol of S ;
A54: x . n in product (Carrier (A,((the_arity_of o) /. n))) by A53, Th15;
then reconsider f4 = x . n as Function ;
A55: x . n in product (Carrier (A,s1)) by A53, A54, PARTFUN1:def_6;
then A56: x . n in (SORTS A) . s1 by PRALG_2:def_10;
dom f4 = dom (Carrier (A,s1)) by A55, CARD_3:9
.= I by PARTFUN1:def_2 ;
then A57: dom (f4 | e) = I /\ e by RELAT_1:61
.= e by XBOOLE_1:28 ;
(F # x) . n in product (Carrier ((product (A / EqR)),((the_arity_of o) /. n))) by A53, Th15;
then reconsider f5 = (F # x) . n as Function ;
consider f7 being Function of ( the Sorts of (product A) . s1),( the Sorts of (product (product (A / EqR))) . s1) such that
A58: f7 = F . s1 and
A59: for x9 being set st x9 in the Sorts of (product A) . s1 holds
S1[f7 . x9,x9,s1] by A15;
f5 = (F . ((the_arity_of o) /. n)) . (x . n) by A53, Th13
.= f7 . (x . n) by A53, A58, PARTFUN1:def_6 ;
then A60: f5 . e = f4 | e by A56, A59;
then reconsider f6 = f5 . e as Function ;
f6 = ((commute (F # x)) . e) . n by A53, Th21;
hence ((commute ((commute (F # x)) . e)) . i1) . n = (f4 | e) . i2 by A47, A48, A53, A60, Th21
.= f4 . i2 by A51, A57, FUNCT_1:47
.= ((commute x) . i1) . n by A53, Th21 ;
::_thesis: verum
end;
(commute x) . i1 is Element of Args (o,(A . i1)) by A40, Th20;
then (commute x) . i1 in Args (o,(A . i1)) ;
then (commute x) . i1 in product ( the Sorts of (A . i1) * (the_arity_of o)) by PRALG_2:3;
then A61: dom ((commute x) . i1) = dom ( the Sorts of (A . i1) * (the_arity_of o)) by CARD_3:9
.= dom (the_arity_of o) by PRALG_2:3 ;
(commute ((commute (F # x)) . e)) . i2 is Element of Args (o,(Cs . i2)) by A40, A47, A48, Th20;
then (commute ((commute (F # x)) . e)) . i2 in Args (o,(Cs . i2)) ;
then (commute ((commute (F # x)) . e)) . i2 in product ( the Sorts of (Cs . i2) * (the_arity_of o)) by PRALG_2:3;
then dom ((commute ((commute (F # x)) . e)) . i1) = dom ( the Sorts of (Cs . i2) * (the_arity_of o)) by CARD_3:9
.= dom (the_arity_of o) by PRALG_2:3 ;
hence (commute ((commute (F # x)) . e)) . i1 = (commute x) . i1 by A61, A52, FUNCT_1:2; ::_thesis: verum
end;
let f2 be Function; ::_thesis: ( f2 = (Den (o,(product A))) . x implies f2 | e = (Den (o,((product (A / EqR)) . e))) . ((commute (F # x)) . e) )
assume A62: f2 = (Den (o,(product A))) . x ; ::_thesis: f2 | e = (Den (o,((product (A / EqR)) . e))) . ((commute (F # x)) . e)
dom f2 = dom (Carrier (A,(the_result_sort_of o))) by A22, A62, CARD_3:9
.= I by PARTFUN1:def_2 ;
then A63: dom (f2 | e) = I /\ e by RELAT_1:61
.= e by XBOOLE_1:28 ;
A64: (commute (F # x)) . e is Element of Args (o,(product Cs)) by A40, A47, Th20;
A65: now__::_thesis:_for_x1_being_set_st_x1_in_e_holds_
f3_._x1_=_(f2_|_e)_._x1
let x1 be set ; ::_thesis: ( x1 in e implies f3 . x1 = (f2 | e) . x1 )
A66: dom (A | e) = (dom A) /\ e by RELAT_1:61
.= I /\ e by PARTFUN1:def_2
.= e by XBOOLE_1:28 ;
assume A67: x1 in e ; ::_thesis: f3 . x1 = (f2 | e) . x1
then reconsider i2 = x1 as Element of Ji by A45, FUNCT_1:18;
reconsider i1 = i2 as Element of I by A67;
Cs = A | e by A46, Def4;
then Cs . i2 = A . i1 by A67, A66, FUNCT_1:47;
hence f3 . x1 = (Den (o,(A . i1))) . ((commute ((commute (F # x)) . e)) . i2) by A40, A47, A64, Th22
.= (Den (o,(A . i1))) . ((commute x) . i1) by A50, A67
.= f2 . x1 by A40, A62, Th22
.= (f2 | e) . x1 by A63, A67, FUNCT_1:47 ;
::_thesis: verum
end;
dom f3 = dom (Carrier (Cs,(the_result_sort_of o))) by A49, CARD_3:9
.= Ji by PARTFUN1:def_2
.= e by A45, FUNCT_1:18 ;
hence f2 | e = (Den (o,((product (A / EqR)) . e))) . ((commute (F # x)) . e) by A63, A65, FUNCT_1:2; ::_thesis: verum
end;
A68: now__::_thesis:_for_x1_being_set_st_x1_in_Class_EqR_holds_
g1_._x1_=_f1_._x1
reconsider f2 = (Den (o,(product A))) . x as Function by A22;
let x1 be set ; ::_thesis: ( x1 in Class EqR implies g1 . x1 = f1 . x1 )
assume x1 in Class EqR ; ::_thesis: g1 . x1 = f1 . x1
then reconsider e = x1 as Element of Class EqR ;
g1 . e = f2 | e by A20, A18;
hence g1 . x1 = (Den (o,((product (A / EqR)) . e))) . ((commute (F # x)) . e) by A44
.= f1 . x1 by A40, Th22 ;
::_thesis: verum
end;
dom g1 = dom (Carrier ((product (A / EqR)),(the_result_sort_of o))) by A19, A43, CARD_3:9
.= Class EqR by PARTFUN1:def_2 ;
hence (F . (the_result_sort_of o)) . ((Den (o,(product A))) . x) = (Den (o,(product (product (A / EqR))))) . (F # x) by A42, A68, FUNCT_1:2; ::_thesis: verum
end;
end;
end;
end;
F is "1-1"
proof
let s be set ; :: according to MSUALG_3:def_2 ::_thesis: for b1 being set holds
( not s in dom F or not F . s = b1 or b1 is one-to-one )
let g be Function; ::_thesis: ( not s in dom F or not F . s = g or g is one-to-one )
assume that
A69: s in dom F and
A70: F . s = g ; ::_thesis: g is one-to-one
consider f being Function of ( the Sorts of (product A) . s),( the Sorts of (product (product (A / EqR))) . s) such that
A71: f = F . s and
A72: for x being set st x in the Sorts of (product A) . s holds
S1[f . x,x,s] by A15, A69;
let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in dom g or not x2 in dom g or not g . x1 = g . x2 or x1 = x2 )
assume that
A73: x1 in dom g and
A74: x2 in dom g and
A75: g . x1 = g . x2 ; ::_thesis: x1 = x2
A76: dom f = dom g by A70, A71;
thus x1 = x2 ::_thesis: verum
proof
reconsider s9 = s as SortSymbol of S by A69;
A77: the Sorts of (product A) . s9 = product (Carrier (A,s9)) by PRALG_2:def_10;
then A78: ex gg being Function st
( x1 = gg & dom gg = dom (Carrier (A,s9)) & ( for x9 being set st x9 in dom (Carrier (A,s9)) holds
gg . x9 in (Carrier (A,s9)) . x9 ) ) by A73, A76, CARD_3:def_5;
A79: ex gg1 being Function st
( x2 = gg1 & dom gg1 = dom (Carrier (A,s9)) & ( for x9 being set st x9 in dom (Carrier (A,s9)) holds
gg1 . x9 in (Carrier (A,s9)) . x9 ) ) by A74, A76, A77, CARD_3:def_5;
reconsider x2 = x2 as Function by A74, A76, A77;
A80: dom x2 = I by A79, PARTFUN1:def_2;
reconsider x1 = x1 as Function by A73, A76, A77;
A81: the Sorts of (product (product (A / EqR))) . s = product (Carrier ((product (A / EqR)),s9)) by PRALG_2:def_10;
A82: for i being set st i in I holds
x1 . i = x2 . i
proof
reconsider f99 = f . x2 as Function by A81;
let i be set ; ::_thesis: ( i in I implies x1 . i = x2 . i )
assume A83: i in I ; ::_thesis: x1 . i = x2 . i
then A84: Class (EqR,i) is Element of Class EqR by EQREL_1:def_3;
then x1 | (Class (EqR,i)) = f99 . (Class (EqR,i)) by A70, A73, A75, A71, A72, A76
.= x2 | (Class (EqR,i)) by A74, A72, A76, A84 ;
then x1 . i = (x2 | (Class (EqR,i))) . i by A83, EQREL_1:20, FUNCT_1:49
.= x2 . i by A83, EQREL_1:20, FUNCT_1:49 ;
hence x1 . i = x2 . i ; ::_thesis: verum
end;
dom x1 = I by A78, PARTFUN1:def_2;
hence x1 = x2 by A80, A82, FUNCT_1:2; ::_thesis: verum
end;
end;
then A85: F is_monomorphism product A, product (product (A / EqR)) by A16, MSUALG_3:def_9;
F is "onto"
proof
let s be set ; :: according to MSUALG_3:def_3 ::_thesis: ( not s in the carrier of S or rng (F . s) = the Sorts of (product (product (A / EqR))) . s )
assume A86: s in the carrier of S ; ::_thesis: rng (F . s) = the Sorts of (product (product (A / EqR))) . s
reconsider s9 = s as SortSymbol of S by A86;
consider f being Function of ( the Sorts of (product A) . s),( the Sorts of (product (product (A / EqR))) . s) such that
A87: f = F . s and
A88: for x being set st x in the Sorts of (product A) . s holds
S1[f . x,x,s] by A15, A86;
A89: the Sorts of (product A) . s9 = product (Carrier (A,s9)) by PRALG_2:def_10;
for y being set holds
( y in the Sorts of (product (product (A / EqR))) . s iff ex x being set st
( x in dom f & y = f . x ) )
proof
let y be set ; ::_thesis: ( y in the Sorts of (product (product (A / EqR))) . s iff ex x being set st
( x in dom f & y = f . x ) )
A90: ( y in the Sorts of (product (product (A / EqR))) . s implies ex x being set st
( x in dom f & y = f . x ) )
proof
assume y in the Sorts of (product (product (A / EqR))) . s ; ::_thesis: ex x being set st
( x in dom f & y = f . x )
then A91: y in product (Carrier ((product (A / EqR)),s9)) by PRALG_2:def_10;
then A92: ex gg being Function st
( y = gg & dom gg = dom (Carrier ((product (A / EqR)),s9)) & ( for x9 being set st x9 in dom (Carrier ((product (A / EqR)),s9)) holds
gg . x9 in (Carrier ((product (A / EqR)),s9)) . x9 ) ) by CARD_3:def_5;
reconsider y = y as Function by A91;
defpred S2[ set , set ] means ex e being Element of Class EqR ex f being Function st
( $1 in e & f = y . e & $2 = f . $1 );
A93: for i being set st i in I holds
ex j being set st S2[i,j]
proof
let i be set ; ::_thesis: ( i in I implies ex j being set st S2[i,j] )
assume A94: i in I ; ::_thesis: ex j being set st S2[i,j]
Class (EqR,i) in Class EqR by A94, EQREL_1:def_3;
then consider e being Element of Class EqR such that
A95: e = Class (EqR,i) ;
consider Ji being non empty set , Cs being MSAlgebra-Family of Ji,S such that
Ji = (id (Class EqR)) . e and
Cs = (A / EqR) . e and
A96: (product (A / EqR)) . e = product Cs by Def5;
ex U0 being MSAlgebra over S st
( U0 = (product (A / EqR)) . e & (Carrier ((product (A / EqR)),s9)) . e = the Sorts of U0 . s9 ) by PRALG_2:def_9;
then ( dom (Carrier ((product (A / EqR)),s9)) = Class EqR & (Carrier ((product (A / EqR)),s9)) . e = product (Carrier (Cs,s9)) ) by A96, PARTFUN1:def_2, PRALG_2:def_10;
then reconsider y9 = y . e as Function by A92, Lm1;
S2[i,y9 . i] by A94, A95, EQREL_1:20;
hence ex j being set st S2[i,j] ; ::_thesis: verum
end;
consider x being ManySortedSet of I such that
A97: for i being set st i in I holds
S2[i,x . i] from PBOOLE:sch_3(A93);
A98: dom (Carrier ((product (A / EqR)),s9)) = Class EqR by PARTFUN1:def_2;
A99: for z being set st z in dom (Carrier (A,s9)) holds
x . z in (Carrier (A,s9)) . z
proof
let z be set ; ::_thesis: ( z in dom (Carrier (A,s9)) implies x . z in (Carrier (A,s9)) . z )
assume z in dom (Carrier (A,s9)) ; ::_thesis: x . z in (Carrier (A,s9)) . z
then z in I ;
then consider e being Element of Class EqR, f1 being Function such that
A100: z in e and
A101: ( f1 = y . e & x . z = f1 . z ) by A97;
dom ((Carrier (A,s9)) | e) = (dom (Carrier (A,s9))) /\ e by RELAT_1:61
.= I /\ e by PARTFUN1:def_2
.= e by XBOOLE_1:28 ;
then A102: ((Carrier (A,s9)) | e) . z = (Carrier (A,s9)) . z by A100, FUNCT_1:47;
consider Ji being non empty set , Cs being MSAlgebra-Family of Ji,S such that
A103: Ji = (id (Class EqR)) . e and
A104: Cs = (A / EqR) . e and
A105: (product (A / EqR)) . e = product Cs by Def5;
( Cs = A | e & Ji = e ) by A103, A104, Def4, FUNCT_1:18;
then A106: Carrier (Cs,s9) = (Carrier (A,s9)) | e by Th2;
ex U0 being MSAlgebra over S st
( U0 = (product (A / EqR)) . e & (Carrier ((product (A / EqR)),s9)) . e = the Sorts of U0 . s9 ) by PRALG_2:def_9;
then A107: (Carrier ((product (A / EqR)),s9)) . e = product (Carrier (Cs,s9)) by A105, PRALG_2:def_10;
y . e in (Carrier ((product (A / EqR)),s9)) . e by A92, A98;
then A108: ex g being Function st
( y . e = g & dom g = dom (Carrier (Cs,s9)) & ( for x9 being set st x9 in dom (Carrier (Cs,s9)) holds
g . x9 in (Carrier (Cs,s9)) . x9 ) ) by A107, CARD_3:def_5;
dom (Carrier (Cs,s9)) = Ji by PARTFUN1:def_2
.= e by A103, FUNCT_1:18 ;
hence x . z in (Carrier (A,s9)) . z by A100, A101, A108, A102, A106; ::_thesis: verum
end;
dom x = I by PARTFUN1:def_2
.= dom (Carrier (A,s9)) by PARTFUN1:def_2 ;
then A109: x in the Sorts of (product A) . s9 by A89, A99, CARD_3:9;
then A110: x in dom f by FUNCT_2:def_1;
then f . x in rng f by FUNCT_1:def_3;
then f . x in the Sorts of (product (product (A / EqR))) . s ;
then A111: f . x in product (Carrier ((product (A / EqR)),s9)) by PRALG_2:def_10;
then reconsider f9 = f . x as Function ;
A112: for e being set st e in Class EqR holds
y . e = f9 . e
proof
let e be set ; ::_thesis: ( e in Class EqR implies y . e = f9 . e )
assume e in Class EqR ; ::_thesis: y . e = f9 . e
then reconsider e = e as Element of Class EqR ;
consider Ji being non empty set , Cs being MSAlgebra-Family of Ji,S such that
A113: Ji = (id (Class EqR)) . e and
Cs = (A / EqR) . e and
A114: (product (A / EqR)) . e = product Cs by Def5;
ex U0 being MSAlgebra over S st
( U0 = (product (A / EqR)) . e & (Carrier ((product (A / EqR)),s9)) . e = the Sorts of U0 . s9 ) by PRALG_2:def_9;
then A115: (Carrier ((product (A / EqR)),s9)) . e = product (Carrier (Cs,s9)) by A114, PRALG_2:def_10;
A116: y . e in (Carrier ((product (A / EqR)),s9)) . e by A92, A98;
then reconsider y9 = y . e as Function by A115;
A117: dom (x | e) = (dom x) /\ e by RELAT_1:61
.= I /\ e by PARTFUN1:def_2
.= e by XBOOLE_1:28 ;
A118: for i being set st i in e holds
(x | e) . i = y9 . i
proof
let i be set ; ::_thesis: ( i in e implies (x | e) . i = y9 . i )
assume A119: i in e ; ::_thesis: (x | e) . i = y9 . i
then consider e1 being Element of Class EqR, f1 being Function such that
A120: i in e1 and
A121: ( f1 = y . e1 & x . i = f1 . i ) by A97;
e = e1 by A119, A120, Th3;
hence (x | e) . i = y9 . i by A117, A119, A121, FUNCT_1:47; ::_thesis: verum
end;
ex g being Function st
( y . e = g & dom g = dom (Carrier (Cs,s9)) & ( for x9 being set st x9 in dom (Carrier (Cs,s9)) holds
g . x9 in (Carrier (Cs,s9)) . x9 ) ) by A116, A115, CARD_3:def_5;
then dom y9 = Ji by PARTFUN1:def_2
.= e by A113, FUNCT_1:18 ;
then x | e = y9 by A117, A118, FUNCT_1:def_11;
hence y . e = f9 . e by A88, A109; ::_thesis: verum
end;
ex gg9 being Function st
( f . x = gg9 & dom gg9 = dom (Carrier ((product (A / EqR)),s9)) & ( for x9 being set st x9 in dom (Carrier ((product (A / EqR)),s9)) holds
gg9 . x9 in (Carrier ((product (A / EqR)),s9)) . x9 ) ) by A111, CARD_3:def_5;
then y = f9 by A92, A98, A112, FUNCT_1:def_11;
hence ex x being set st
( x in dom f & y = f . x ) by A110; ::_thesis: verum
end;
( ex x being set st
( x in dom f & y = f . x ) implies y in the Sorts of (product (product (A / EqR))) . s )
proof
given x being set such that A122: x in dom f and
A123: y = f . x ; ::_thesis: y in the Sorts of (product (product (A / EqR))) . s
f . x in rng f by A122, FUNCT_1:def_3;
hence y in the Sorts of (product (product (A / EqR))) . s by A123; ::_thesis: verum
end;
hence ( y in the Sorts of (product (product (A / EqR))) . s iff ex x being set st
( x in dom f & y = f . x ) ) by A90; ::_thesis: verum
end;
hence rng (F . s) = the Sorts of (product (product (A / EqR))) . s by A87, FUNCT_1:def_3; ::_thesis: verum
end;
then F is_epimorphism product A, product (product (A / EqR)) by A16, MSUALG_3:def_8;
then F is_isomorphism product A, product (product (A / EqR)) by A85, MSUALG_3:def_10;
hence product A, product (product (A / EqR)) are_isomorphic by MSUALG_3:def_11; ::_thesis: verum
end;