:: OSALG_4 semantic presentation
begin
registration
let R be non empty Poset;
cluster non empty Relation-like the carrier of R -defined Function-like total Relation-yielding order-sorted for set ;
existence
ex b1 being OrderSortedSet of R st b1 is Relation-yielding
proof
set R1 = the Relation;
set I = the carrier of R;
set f = the carrier of R --> the Relation;
reconsider f = the carrier of R --> the Relation as ManySortedSet of the carrier of R ;
f is order-sorted
proof
let s1, s2 be Element of R; :: according to OSALG_1:def_16 ::_thesis: ( not s1 <= s2 or f . s1 c= f . s2 )
assume s1 <= s2 ; ::_thesis: f . s1 c= f . s2
f . s1 = the Relation by FUNCOP_1:7;
hence f . s1 c= f . s2 by FUNCOP_1:7; ::_thesis: verum
end;
then reconsider f = f as OrderSortedSet of R ;
take f ; ::_thesis: f is Relation-yielding
for x being set st x in dom f holds
f . x is Relation by FUNCOP_1:7;
hence f is Relation-yielding by FUNCOP_1:def_11; ::_thesis: verum
end;
end;
definition
let R be non empty Poset;
let A, B be ManySortedSet of the carrier of R;
let IT be ManySortedRelation of A,B;
attrIT is os-compatible means :Def1: :: OSALG_4:def 1
for s1, s2 being Element of R st s1 <= s2 holds
for x, y being set st x in A . s1 & y in B . s1 holds
( [x,y] in IT . s1 iff [x,y] in IT . s2 );
end;
:: deftheorem Def1 defines os-compatible OSALG_4:def_1_:_
for R being non empty Poset
for A, B being ManySortedSet of the carrier of R
for IT being ManySortedRelation of A,B holds
( IT is os-compatible iff for s1, s2 being Element of R st s1 <= s2 holds
for x, y being set st x in A . s1 & y in B . s1 holds
( [x,y] in IT . s1 iff [x,y] in IT . s2 ) );
registration
let R be non empty Poset;
let A, B be ManySortedSet of the carrier of R;
cluster non empty Relation-like the carrier of R -defined Function-like total Relation-yielding os-compatible for ManySortedRelation of A,B;
existence
ex b1 being ManySortedRelation of A,B st b1 is os-compatible
proof
set I = the carrier of R;
consider R1 being Relation such that
A1: R1 = {} ;
set f = the carrier of R --> R1;
reconsider f = the carrier of R --> R1 as ManySortedSet of R ;
set f1 = f;
for i being set st i in the carrier of R holds
f . i is Relation of (A . i),(B . i)
proof
let i be set ; ::_thesis: ( i in the carrier of R implies f . i is Relation of (A . i),(B . i) )
assume i in the carrier of R ; ::_thesis: f . i is Relation of (A . i),(B . i)
then f . i = {} by A1, FUNCOP_1:7;
hence f . i is Relation of (A . i),(B . i) by RELSET_1:12; ::_thesis: verum
end;
then reconsider f2 = f as ManySortedRelation of A,B by MSUALG_4:def_1;
take f ; ::_thesis: ( f is ManySortedRelation of A,B & f is os-compatible )
for s1, s2 being Element of R st s1 <= s2 holds
for x, y being set st x in A . s1 & y in B . s1 holds
( [x,y] in f . s1 iff [x,y] in f . s2 )
proof
let s1, s2 be Element of R; ::_thesis: ( s1 <= s2 implies for x, y being set st x in A . s1 & y in B . s1 holds
( [x,y] in f . s1 iff [x,y] in f . s2 ) )
assume s1 <= s2 ; ::_thesis: for x, y being set st x in A . s1 & y in B . s1 holds
( [x,y] in f . s1 iff [x,y] in f . s2 )
let x, y be set ; ::_thesis: ( x in A . s1 & y in B . s1 implies ( [x,y] in f . s1 iff [x,y] in f . s2 ) )
assume that
x in A . s1 and
y in B . s1 ; ::_thesis: ( [x,y] in f . s1 iff [x,y] in f . s2 )
f . s1 = R1 by FUNCOP_1:7
.= f . s2 by FUNCOP_1:7 ;
hence ( [x,y] in f . s1 iff [x,y] in f . s2 ) ; ::_thesis: verum
end;
then f2 is os-compatible by Def1;
hence ( f is ManySortedRelation of A,B & f is os-compatible ) ; ::_thesis: verum
end;
end;
definition
let R be non empty Poset;
let A, B be ManySortedSet of the carrier of R;
mode OrderSortedRelation of A,B is os-compatible ManySortedRelation of A,B;
end;
theorem Th1: :: OSALG_4:1
for R being non empty Poset
for A, B being ManySortedSet of the carrier of R
for OR being ManySortedRelation of A,B st OR is os-compatible holds
OR is OrderSortedSet of R
proof
let R be non empty Poset; ::_thesis: for A, B being ManySortedSet of the carrier of R
for OR being ManySortedRelation of A,B st OR is os-compatible holds
OR is OrderSortedSet of R
let A, B be ManySortedSet of the carrier of R; ::_thesis: for OR being ManySortedRelation of A,B st OR is os-compatible holds
OR is OrderSortedSet of R
let OR be ManySortedRelation of A,B; ::_thesis: ( OR is os-compatible implies OR is OrderSortedSet of R )
set OR1 = OR;
assume A1: OR is os-compatible ; ::_thesis: OR is OrderSortedSet of R
OR is order-sorted
proof
let s1, s2 be Element of R; :: according to OSALG_1:def_16 ::_thesis: ( not s1 <= s2 or OR . s1 c= OR . s2 )
assume A2: s1 <= s2 ; ::_thesis: OR . s1 c= OR . s2
for x, y being set st [x,y] in OR . s1 holds
[x,y] in OR . s2
proof
let x, y be set ; ::_thesis: ( [x,y] in OR . s1 implies [x,y] in OR . s2 )
assume A3: [x,y] in OR . s1 ; ::_thesis: [x,y] in OR . s2
( x in A . s1 & y in B . s1 ) by A3, ZFMISC_1:87;
hence [x,y] in OR . s2 by A1, A2, A3, Def1; ::_thesis: verum
end;
hence OR . s1 c= OR . s2 by RELAT_1:def_3; ::_thesis: verum
end;
hence OR is OrderSortedSet of R ; ::_thesis: verum
end;
registration
let R be non empty Poset;
let A, B be ManySortedSet of R;
cluster os-compatible -> order-sorted for ManySortedRelation of A,B;
coherence
for b1 being ManySortedRelation of A,B st b1 is os-compatible holds
b1 is order-sorted by Th1;
end;
definition
let R be non empty Poset;
let A be ManySortedSet of the carrier of R;
mode OrderSortedRelation of A is OrderSortedRelation of A,A;
end;
definition
let S be OrderSortedSign;
let U1 be OSAlgebra of S;
mode OrderSortedRelation of U1 -> ManySortedRelation of U1 means :Def2: :: OSALG_4:def 2
it is os-compatible ;
existence
ex b1 being ManySortedRelation of U1 st b1 is os-compatible
proof
reconsider Y = the Sorts of U1 as OrderSortedSet of S by OSALG_1:17;
set X = the OrderSortedRelation of Y;
reconsider X1 = the OrderSortedRelation of Y as ManySortedRelation of U1 ;
take X1 ; ::_thesis: X1 is os-compatible
thus X1 is os-compatible ; ::_thesis: verum
end;
end;
:: deftheorem Def2 defines OrderSortedRelation OSALG_4:def_2_:_
for S being OrderSortedSign
for U1 being OSAlgebra of S
for b3 being ManySortedRelation of U1 holds
( b3 is OrderSortedRelation of U1 iff b3 is os-compatible );
registration
let S be OrderSortedSign;
let U1 be OSAlgebra of S;
cluster non empty Relation-like the carrier of S -defined Function-like total Relation-yielding MSEquivalence-like for OrderSortedRelation of U1;
existence
ex b1 being OrderSortedRelation of U1 st b1 is MSEquivalence-like
proof
deffunc H1( Element of S) -> Element of bool [:( the Sorts of U1 . S),( the Sorts of U1 . S):] = id ( the Sorts of U1 . S);
consider f being Function such that
A1: ( dom f = the carrier of S & ( for d being Element of S holds f . d = H1(d) ) ) from FUNCT_1:sch_4();
reconsider f = f as ManySortedSet of the carrier of S by A1, PARTFUN1:def_2, RELAT_1:def_18;
for i being set st i in the carrier of S holds
f . i is Relation of ( the Sorts of U1 . i),( the Sorts of U1 . i)
proof
let i be set ; ::_thesis: ( i in the carrier of S implies f . i is Relation of ( the Sorts of U1 . i),( the Sorts of U1 . i) )
assume i in the carrier of S ; ::_thesis: f . i is Relation of ( the Sorts of U1 . i),( the Sorts of U1 . i)
then f . i = id ( the Sorts of U1 . i) by A1;
hence f . i is Relation of ( the Sorts of U1 . i),( the Sorts of U1 . i) ; ::_thesis: verum
end;
then reconsider f = f as ManySortedRelation of the Sorts of U1, the Sorts of U1 by MSUALG_4:def_1;
reconsider f = f as ManySortedRelation of U1 ;
set f1 = f;
A2: f is os-compatible
proof
reconsider X = the Sorts of U1 as OrderSortedSet of S by OSALG_1:17;
let s1, s2 be Element of S; :: according to OSALG_4:def_1 ::_thesis: ( s1 <= s2 implies for x, y being set st x in the Sorts of U1 . s1 & y in the Sorts of U1 . s1 holds
( [x,y] in f . s1 iff [x,y] in f . s2 ) )
assume A3: s1 <= s2 ; ::_thesis: for x, y being set st x in the Sorts of U1 . s1 & y in the Sorts of U1 . s1 holds
( [x,y] in f . s1 iff [x,y] in f . s2 )
reconsider s3 = s1, s4 = s2 as Element of S ;
let x, y be set ; ::_thesis: ( x in the Sorts of U1 . s1 & y in the Sorts of U1 . s1 implies ( [x,y] in f . s1 iff [x,y] in f . s2 ) )
assume that
A4: x in the Sorts of U1 . s1 and
y in the Sorts of U1 . s1 ; ::_thesis: ( [x,y] in f . s1 iff [x,y] in f . s2 )
A5: f . s1 = id (X . s1) by A1;
A6: f . s2 = id (X . s2) by A1;
X . s3 c= X . s4 by A3, OSALG_1:def_16;
then id (X . s1) c= id (X . s2) by SYSREL:15;
hence ( [x,y] in f . s1 implies [x,y] in f . s2 ) by A5, A6; ::_thesis: ( [x,y] in f . s2 implies [x,y] in f . s1 )
assume [x,y] in f . s2 ; ::_thesis: [x,y] in f . s1
then x = y by A6, RELAT_1:def_10;
hence [x,y] in f . s1 by A5, A4, RELAT_1:def_10; ::_thesis: verum
end;
take f ; ::_thesis: ( f is OrderSortedRelation of U1 & f is MSEquivalence-like )
for i being set
for R being Relation of ( the Sorts of U1 . i) st i in the carrier of S & f . i = R holds
R is Equivalence_Relation of ( the Sorts of U1 . i)
proof
let i be set ; ::_thesis: for R being Relation of ( the Sorts of U1 . i) st i in the carrier of S & f . i = R holds
R is Equivalence_Relation of ( the Sorts of U1 . i)
let R be Relation of ( the Sorts of U1 . i); ::_thesis: ( i in the carrier of S & f . i = R implies R is Equivalence_Relation of ( the Sorts of U1 . i) )
assume ( i in the carrier of S & f . i = R ) ; ::_thesis: R is Equivalence_Relation of ( the Sorts of U1 . i)
then R = id ( the Sorts of U1 . i) by A1;
hence R is Equivalence_Relation of ( the Sorts of U1 . i) ; ::_thesis: verum
end;
then f is MSEquivalence_Relation-like by MSUALG_4:def_2;
hence ( f is OrderSortedRelation of U1 & f is MSEquivalence-like ) by A2, Def2, MSUALG_4:def_3; ::_thesis: verum
end;
end;
registration
let S be OrderSortedSign;
let U1 be non-empty OSAlgebra of S;
cluster non empty Relation-like the carrier of S -defined Function-like total Relation-yielding MSEquivalence-like MSCongruence-like for OrderSortedRelation of U1;
existence
ex b1 being MSEquivalence-like OrderSortedRelation of U1 st b1 is MSCongruence-like
proof
deffunc H1( Element of S) -> Element of bool [:( the Sorts of U1 . S),( the Sorts of U1 . S):] = id ( the Sorts of U1 . S);
consider f being Function such that
A1: ( dom f = the carrier of S & ( for d being Element of S holds f . d = H1(d) ) ) from FUNCT_1:sch_4();
reconsider f = f as ManySortedSet of the carrier of S by A1, PARTFUN1:def_2, RELAT_1:def_18;
for i being set st i in the carrier of S holds
f . i is Relation of ( the Sorts of U1 . i),( the Sorts of U1 . i)
proof
let i be set ; ::_thesis: ( i in the carrier of S implies f . i is Relation of ( the Sorts of U1 . i),( the Sorts of U1 . i) )
assume i in the carrier of S ; ::_thesis: f . i is Relation of ( the Sorts of U1 . i),( the Sorts of U1 . i)
then f . i = id ( the Sorts of U1 . i) by A1;
hence f . i is Relation of ( the Sorts of U1 . i),( the Sorts of U1 . i) ; ::_thesis: verum
end;
then reconsider f = f as ManySortedRelation of the Sorts of U1, the Sorts of U1 by MSUALG_4:def_1;
reconsider f = f as ManySortedRelation of U1 ;
for i being set
for R being Relation of ( the Sorts of U1 . i) st i in the carrier of S & f . i = R holds
R is Equivalence_Relation of ( the Sorts of U1 . i)
proof
let i be set ; ::_thesis: for R being Relation of ( the Sorts of U1 . i) st i in the carrier of S & f . i = R holds
R is Equivalence_Relation of ( the Sorts of U1 . i)
let R be Relation of ( the Sorts of U1 . i); ::_thesis: ( i in the carrier of S & f . i = R implies R is Equivalence_Relation of ( the Sorts of U1 . i) )
assume ( i in the carrier of S & f . i = R ) ; ::_thesis: R is Equivalence_Relation of ( the Sorts of U1 . i)
then R = id ( the Sorts of U1 . i) by A1;
hence R is Equivalence_Relation of ( the Sorts of U1 . i) ; ::_thesis: verum
end;
then f is MSEquivalence_Relation-like by MSUALG_4:def_2;
then reconsider f = f as MSEquivalence-like ManySortedRelation of U1 by MSUALG_4:def_3;
set f1 = f;
f is os-compatible
proof
reconsider X = the Sorts of U1 as OrderSortedSet of S by OSALG_1:17;
let s1, s2 be Element of S; :: according to OSALG_4:def_1 ::_thesis: ( s1 <= s2 implies for x, y being set st x in the Sorts of U1 . s1 & y in the Sorts of U1 . s1 holds
( [x,y] in f . s1 iff [x,y] in f . s2 ) )
assume A2: s1 <= s2 ; ::_thesis: for x, y being set st x in the Sorts of U1 . s1 & y in the Sorts of U1 . s1 holds
( [x,y] in f . s1 iff [x,y] in f . s2 )
reconsider s3 = s1, s4 = s2 as Element of S ;
let x, y be set ; ::_thesis: ( x in the Sorts of U1 . s1 & y in the Sorts of U1 . s1 implies ( [x,y] in f . s1 iff [x,y] in f . s2 ) )
assume that
A3: x in the Sorts of U1 . s1 and
y in the Sorts of U1 . s1 ; ::_thesis: ( [x,y] in f . s1 iff [x,y] in f . s2 )
A4: f . s1 = id (X . s1) by A1;
A5: f . s2 = id (X . s2) by A1;
X . s3 c= X . s4 by A2, OSALG_1:def_16;
then id (X . s1) c= id (X . s2) by SYSREL:15;
hence ( [x,y] in f . s1 implies [x,y] in f . s2 ) by A4, A5; ::_thesis: ( [x,y] in f . s2 implies [x,y] in f . s1 )
assume [x,y] in f . s2 ; ::_thesis: [x,y] in f . s1
then x = y by A5, RELAT_1:def_10;
hence [x,y] in f . s1 by A4, A3, RELAT_1:def_10; ::_thesis: verum
end;
then reconsider f = f as MSEquivalence-like OrderSortedRelation of U1 by Def2;
take f ; ::_thesis: f is MSCongruence-like
for o being Element of the carrier' of S
for x, y being Element of Args (o,U1) st ( for n being Nat st n in dom x holds
[(x . n),(y . n)] in f . ((the_arity_of o) /. n) ) holds
[((Den (o,U1)) . x),((Den (o,U1)) . y)] in f . (the_result_sort_of o)
proof
let o be Element of the carrier' of S; ::_thesis: for x, y being Element of Args (o,U1) st ( for n being Nat st n in dom x holds
[(x . n),(y . n)] in f . ((the_arity_of o) /. n) ) holds
[((Den (o,U1)) . x),((Den (o,U1)) . y)] in f . (the_result_sort_of o)
let x, y be Element of Args (o,U1); ::_thesis: ( ( for n being Nat st n in dom x holds
[(x . n),(y . n)] in f . ((the_arity_of o) /. n) ) implies [((Den (o,U1)) . x),((Den (o,U1)) . y)] in f . (the_result_sort_of o) )
A6: dom x = dom (the_arity_of o) by MSUALG_3:6;
assume A7: for n being Nat st n in dom x holds
[(x . n),(y . n)] in f . ((the_arity_of o) /. n) ; ::_thesis: [((Den (o,U1)) . x),((Den (o,U1)) . y)] in f . (the_result_sort_of o)
A8: for a being set st a in dom (the_arity_of o) holds
x . a = y . a
proof
set ao = the_arity_of o;
let a be set ; ::_thesis: ( a in dom (the_arity_of o) implies x . a = y . a )
assume A9: a in dom (the_arity_of o) ; ::_thesis: x . a = y . a
then reconsider n = a as Nat ;
(the_arity_of o) . n in rng (the_arity_of o) by A9, FUNCT_1:def_3;
then A10: f . ((the_arity_of o) . n) = id ( the Sorts of U1 . ((the_arity_of o) . n)) by A1;
(the_arity_of o) /. n = (the_arity_of o) . n by A9, PARTFUN1:def_6;
then [(x . n),(y . n)] in f . ((the_arity_of o) . n) by A7, A6, A9;
hence x . a = y . a by A10, RELAT_1:def_10; ::_thesis: verum
end;
set r = the_result_sort_of o;
A11: f . (the_result_sort_of o) = id ( the Sorts of U1 . (the_result_sort_of o)) by A1;
A12: dom the ResultSort of S = the carrier' of S by FUNCT_2:def_1;
then A13: dom ( the Sorts of U1 * the ResultSort of S) = dom the ResultSort of S by PARTFUN1:def_2;
A14: Result (o,U1) = ( the Sorts of U1 * the ResultSort of S) . o by MSUALG_1:def_5
.= the Sorts of U1 . ( the ResultSort of S . o) by A12, A13, FUNCT_1:12
.= the Sorts of U1 . (the_result_sort_of o) by MSUALG_1:def_2 ;
dom y = dom (the_arity_of o) by MSUALG_3:6;
then (Den (o,U1)) . x = (Den (o,U1)) . y by A6, A8, FUNCT_1:2;
hence [((Den (o,U1)) . x),((Den (o,U1)) . y)] in f . (the_result_sort_of o) by A11, A14, RELAT_1:def_10; ::_thesis: verum
end;
hence f is MSCongruence-like by MSUALG_4:def_4; ::_thesis: verum
end;
end;
definition
let S be OrderSortedSign;
let U1 be non-empty OSAlgebra of S;
mode OSCongruence of U1 is MSEquivalence-like MSCongruence-like OrderSortedRelation of U1;
end;
definition
let R be non empty Poset;
func Path_Rel R -> Equivalence_Relation of the carrier of R means :Def3: :: OSALG_4:def 3
for x, y being set holds
( [x,y] in it iff ( x in the carrier of R & y in the carrier of R & ex p being FinSequence of the carrier of R st
( 1 < len p & p . 1 = x & p . (len p) = y & ( for n being Nat st 2 <= n & n <= len p & not [(p . n),(p . (n - 1))] in the InternalRel of R holds
[(p . (n - 1)),(p . n)] in the InternalRel of R ) ) ) );
existence
ex b1 being Equivalence_Relation of the carrier of R st
for x, y being set holds
( [x,y] in b1 iff ( x in the carrier of R & y in the carrier of R & ex p being FinSequence of the carrier of R st
( 1 < len p & p . 1 = x & p . (len p) = y & ( for n being Nat st 2 <= n & n <= len p & not [(p . n),(p . (n - 1))] in the InternalRel of R holds
[(p . (n - 1)),(p . n)] in the InternalRel of R ) ) ) )
proof
defpred S1[ set , set ] means ex p being FinSequence of the carrier of R st
( 1 < len p & p . 1 = $1 & p . (len p) = $2 & ( for n being Nat st 2 <= n & n <= len p & not [(p . n),(p . (n - 1))] in the InternalRel of R holds
[(p . (n - 1)),(p . n)] in the InternalRel of R ) );
set P = { [x,y] where x, y is Element of R : ( x in the carrier of R & y in the carrier of R & S1[x,y] ) } ;
{ [x,y] where x, y is Element of R : ( x in the carrier of R & y in the carrier of R & S1[x,y] ) } c= [: the carrier of R, the carrier of R:]
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { [x,y] where x, y is Element of R : ( x in the carrier of R & y in the carrier of R & S1[x,y] ) } or z in [: the carrier of R, the carrier of R:] )
assume z in { [x,y] where x, y is Element of R : ( x in the carrier of R & y in the carrier of R & S1[x,y] ) } ; ::_thesis: z in [: the carrier of R, the carrier of R:]
then ex x, y being Element of R st
( z = [x,y] & x in the carrier of R & y in the carrier of R & S1[x,y] ) ;
hence z in [: the carrier of R, the carrier of R:] by ZFMISC_1:87; ::_thesis: verum
end;
then reconsider P1 = { [x,y] where x, y is Element of R : ( x in the carrier of R & y in the carrier of R & S1[x,y] ) } as Relation of the carrier of R ;
A1: for x, y being set holds
( [x,y] in { [x,y] where x, y is Element of R : ( x in the carrier of R & y in the carrier of R & S1[x,y] ) } iff ( x in the carrier of R & y in the carrier of R & S1[x,y] ) )
proof
let x, y be set ; ::_thesis: ( [x,y] in { [x,y] where x, y is Element of R : ( x in the carrier of R & y in the carrier of R & S1[x,y] ) } iff ( x in the carrier of R & y in the carrier of R & S1[x,y] ) )
hereby ::_thesis: ( x in the carrier of R & y in the carrier of R & S1[x,y] implies [x,y] in { [x,y] where x, y is Element of R : ( x in the carrier of R & y in the carrier of R & S1[x,y] ) } )
assume [x,y] in { [x,y] where x, y is Element of R : ( x in the carrier of R & y in the carrier of R & S1[x,y] ) } ; ::_thesis: ( x in the carrier of R & y in the carrier of R & S1[x,y] )
then consider x1, y1 being Element of R such that
A2: [x,y] = [x1,y1] and
x1 in the carrier of R and
y1 in the carrier of R and
A3: S1[x1,y1] ;
( x = x1 & y = y1 ) by A2, XTUPLE_0:1;
hence ( x in the carrier of R & y in the carrier of R & S1[x,y] ) by A3; ::_thesis: verum
end;
thus ( x in the carrier of R & y in the carrier of R & S1[x,y] implies [x,y] in { [x,y] where x, y is Element of R : ( x in the carrier of R & y in the carrier of R & S1[x,y] ) } ) ; ::_thesis: verum
end;
now__::_thesis:_for_x,_y_being_set_st_x_in_the_carrier_of_R_&_y_in_the_carrier_of_R_&_[x,y]_in_P1_holds_
[y,x]_in_P1
let x, y be set ; ::_thesis: ( x in the carrier of R & y in the carrier of R & [x,y] in P1 implies [y,x] in P1 )
assume that
A4: ( x in the carrier of R & y in the carrier of R ) and
A5: [x,y] in P1 ; ::_thesis: [y,x] in P1
consider p being FinSequence of the carrier of R such that
A6: 1 < len p and
A7: ( p . 1 = x & p . (len p) = y ) and
A8: for n being Nat st 2 <= n & n <= len p & not [(p . n),(p . (n - 1))] in the InternalRel of R holds
[(p . (n - 1)),(p . n)] in the InternalRel of R by A1, A5;
S1[y,x]
proof
take F = Rev p; ::_thesis: ( 1 < len F & F . 1 = y & F . (len F) = x & ( for n being Nat st 2 <= n & n <= len F & not [(F . n),(F . (n - 1))] in the InternalRel of R holds
[(F . (n - 1)),(F . n)] in the InternalRel of R ) )
thus 1 < len F by A6, FINSEQ_5:def_3; ::_thesis: ( F . 1 = y & F . (len F) = x & ( for n being Nat st 2 <= n & n <= len F & not [(F . n),(F . (n - 1))] in the InternalRel of R holds
[(F . (n - 1)),(F . n)] in the InternalRel of R ) )
A9: len F = len p by FINSEQ_5:def_3;
hence ( F . 1 = y & F . (len F) = x ) by A7, FINSEQ_5:62; ::_thesis: for n being Nat st 2 <= n & n <= len F & not [(F . n),(F . (n - 1))] in the InternalRel of R holds
[(F . (n - 1)),(F . n)] in the InternalRel of R
let n1 be Nat; ::_thesis: ( 2 <= n1 & n1 <= len F & not [(F . n1),(F . (n1 - 1))] in the InternalRel of R implies [(F . (n1 - 1)),(F . n1)] in the InternalRel of R )
assume that
A10: 2 <= n1 and
A11: n1 <= len F ; ::_thesis: ( [(F . n1),(F . (n1 - 1))] in the InternalRel of R or [(F . (n1 - 1)),(F . n1)] in the InternalRel of R )
1 <= n1 by A10, XXREAL_0:2;
then A12: n1 in dom p by A9, A11, FINSEQ_3:25;
set n2 = ((len p) - n1) + 2;
0 <= (len p) - n1 by A9, A11, XREAL_1:48;
then A13: 2 + 0 <= ((len p) - n1) + 2 by XREAL_1:6;
A14: 2 - 1 <= n1 - 1 by A10, XREAL_1:9;
then reconsider n11 = n1 - 1 as Element of NAT by INT_1:3, XXREAL_0:2;
n1 - 1 <= (len F) - 0 by A11, XREAL_1:13;
then n11 in dom p by A9, A14, FINSEQ_3:25;
then A15: F . (n1 - 1) = p . (((len p) - (n1 - 1)) + 1) by FINSEQ_5:58
.= p . (((len p) - n1) + 2) ;
reconsider n2 = ((len p) - n1) + 2 as Element of NAT by A13, INT_1:3, XXREAL_0:2;
(len p) - n1 <= (len p) - 2 by A10, XREAL_1:13;
then A16: ((len p) - n1) + 2 <= ((len p) - 2) + 2 by XREAL_1:6;
p . (n2 - 1) = p . (((len p) - n1) + (2 - 1))
.= F . n1 by A12, FINSEQ_5:58 ;
hence ( [(F . n1),(F . (n1 - 1))] in the InternalRel of R or [(F . (n1 - 1)),(F . n1)] in the InternalRel of R ) by A8, A15, A13, A16; ::_thesis: verum
end;
hence [y,x] in P1 by A4; ::_thesis: verum
end;
then A17: P1 is_symmetric_in the carrier of R by RELAT_2:def_3;
A18: the InternalRel of R is_reflexive_in the carrier of R by ORDERS_2:def_2;
now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_R_holds_
[x,x]_in_P1
let x be set ; ::_thesis: ( x in the carrier of R implies [x,x] in P1 )
assume A19: x in the carrier of R ; ::_thesis: [x,x] in P1
S1[x,x]
proof
set F = <*x,x*>;
rng <*x,x*> = {x,x} by FINSEQ_2:127
.= {x} by ENUMSET1:29 ;
then rng <*x,x*> c= the carrier of R by A19, ZFMISC_1:31;
then reconsider F1 = <*x,x*> as FinSequence of the carrier of R by FINSEQ_1:def_4;
take F1 ; ::_thesis: ( 1 < len F1 & F1 . 1 = x & F1 . (len F1) = x & ( for n being Nat st 2 <= n & n <= len F1 & not [(F1 . n),(F1 . (n - 1))] in the InternalRel of R holds
[(F1 . (n - 1)),(F1 . n)] in the InternalRel of R ) )
A20: len <*x,x*> = 2 by FINSEQ_1:44;
hence 1 < len F1 ; ::_thesis: ( F1 . 1 = x & F1 . (len F1) = x & ( for n being Nat st 2 <= n & n <= len F1 & not [(F1 . n),(F1 . (n - 1))] in the InternalRel of R holds
[(F1 . (n - 1)),(F1 . n)] in the InternalRel of R ) )
thus ( F1 . 1 = x & F1 . (len F1) = x ) by A20, FINSEQ_1:44; ::_thesis: for n being Nat st 2 <= n & n <= len F1 & not [(F1 . n),(F1 . (n - 1))] in the InternalRel of R holds
[(F1 . (n - 1)),(F1 . n)] in the InternalRel of R
let n1 be Nat; ::_thesis: ( 2 <= n1 & n1 <= len F1 & not [(F1 . n1),(F1 . (n1 - 1))] in the InternalRel of R implies [(F1 . (n1 - 1)),(F1 . n1)] in the InternalRel of R )
assume ( 2 <= n1 & n1 <= len F1 ) ; ::_thesis: ( [(F1 . n1),(F1 . (n1 - 1))] in the InternalRel of R or [(F1 . (n1 - 1)),(F1 . n1)] in the InternalRel of R )
then A21: n1 = 2 by A20, XXREAL_0:1;
( <*x,x*> . 1 = x & <*x,x*> . 2 = x ) by FINSEQ_1:44;
hence ( [(F1 . n1),(F1 . (n1 - 1))] in the InternalRel of R or [(F1 . (n1 - 1)),(F1 . n1)] in the InternalRel of R ) by A18, A19, A21, RELAT_2:def_1; ::_thesis: verum
end;
hence [x,x] in P1 by A19; ::_thesis: verum
end;
then P1 is_reflexive_in the carrier of R by RELAT_2:def_1;
then A22: ( dom P1 = the carrier of R & field P1 = the carrier of R ) by ORDERS_1:13;
now__::_thesis:_for_x,_y,_z_being_set_st_x_in_the_carrier_of_R_&_y_in_the_carrier_of_R_&_z_in_the_carrier_of_R_&_[x,y]_in_P1_&_[y,z]_in_P1_holds_
[x,z]_in_P1
let x, y, z be set ; ::_thesis: ( x in the carrier of R & y in the carrier of R & z in the carrier of R & [x,y] in P1 & [y,z] in P1 implies [x,z] in P1 )
assume that
A23: x in the carrier of R and
A24: y in the carrier of R and
A25: z in the carrier of R and
A26: ( [x,y] in P1 & [y,z] in P1 ) ; ::_thesis: [x,z] in P1
( S1[x,y] & S1[y,z] ) by A1, A26;
then consider p1, p2 being FinSequence of the carrier of R such that
A27: 1 < len p1 and
A28: p1 . 1 = x and
A29: p1 . (len p1) = y and
A30: for n being Nat st 2 <= n & n <= len p1 & not [(p1 . n),(p1 . (n - 1))] in the InternalRel of R holds
[(p1 . (n - 1)),(p1 . n)] in the InternalRel of R and
A31: 1 < len p2 and
A32: p2 . 1 = y and
A33: p2 . (len p2) = z and
A34: for n being Nat st 2 <= n & n <= len p2 & not [(p2 . n),(p2 . (n - 1))] in the InternalRel of R holds
[(p2 . (n - 1)),(p2 . n)] in the InternalRel of R ;
S1[x,z]
proof
take F = p1 ^ p2; ::_thesis: ( 1 < len F & F . 1 = x & F . (len F) = z & ( for n being Nat st 2 <= n & n <= len F & not [(F . n),(F . (n - 1))] in the InternalRel of R holds
[(F . (n - 1)),(F . n)] in the InternalRel of R ) )
A35: len F = (len p1) + (len p2) by FINSEQ_1:22;
1 + 1 < (len p1) + (len p2) by A27, A31, XREAL_1:8;
hence 1 < len F by A35, XXREAL_0:2; ::_thesis: ( F . 1 = x & F . (len F) = z & ( for n being Nat st 2 <= n & n <= len F & not [(F . n),(F . (n - 1))] in the InternalRel of R holds
[(F . (n - 1)),(F . n)] in the InternalRel of R ) )
1 in dom p1 by A27, FINSEQ_3:25;
hence F . 1 = x by A28, FINSEQ_1:def_7; ::_thesis: ( F . (len F) = z & ( for n being Nat st 2 <= n & n <= len F & not [(F . n),(F . (n - 1))] in the InternalRel of R holds
[(F . (n - 1)),(F . n)] in the InternalRel of R ) )
len p2 in dom p2 by A31, FINSEQ_3:25;
hence F . (len F) = z by A33, A35, FINSEQ_1:def_7; ::_thesis: for n being Nat st 2 <= n & n <= len F & not [(F . n),(F . (n - 1))] in the InternalRel of R holds
[(F . (n - 1)),(F . n)] in the InternalRel of R
let n1 be Nat; ::_thesis: ( 2 <= n1 & n1 <= len F & not [(F . n1),(F . (n1 - 1))] in the InternalRel of R implies [(F . (n1 - 1)),(F . n1)] in the InternalRel of R )
assume that
A36: 2 <= n1 and
A37: n1 <= len F ; ::_thesis: ( [(F . n1),(F . (n1 - 1))] in the InternalRel of R or [(F . (n1 - 1)),(F . n1)] in the InternalRel of R )
A38: 1 <= n1 by A36, XXREAL_0:2;
A39: 2 - 1 <= n1 - 1 by A36, XREAL_1:9;
then reconsider n11 = n1 - 1 as Element of NAT by INT_1:3, XXREAL_0:2;
A40: ( not (len p1) + 1 <= n1 or (len p1) + 1 = n1 or (len p1) + 1 < n1 ) by XXREAL_0:1;
A41: n1 - 1 <= (len F) - 0 by A37, XREAL_1:13;
percases ( n1 <= len p1 or (len p1) + 1 < n1 or (len p1) + 1 = n1 ) by A40, INT_1:7;
supposeA42: n1 <= len p1 ; ::_thesis: ( [(F . n1),(F . (n1 - 1))] in the InternalRel of R or [(F . (n1 - 1)),(F . n1)] in the InternalRel of R )
then n1 - 1 <= (len p1) - 0 by XREAL_1:13;
then n11 in dom p1 by A39, FINSEQ_3:25;
then A43: F . (n1 - 1) = p1 . (n1 - 1) by FINSEQ_1:def_7;
n1 in dom p1 by A38, A42, FINSEQ_3:25;
then F . n1 = p1 . n1 by FINSEQ_1:def_7;
hence ( [(F . n1),(F . (n1 - 1))] in the InternalRel of R or [(F . (n1 - 1)),(F . n1)] in the InternalRel of R ) by A30, A36, A42, A43; ::_thesis: verum
end;
supposeA44: (len p1) + 1 < n1 ; ::_thesis: ( [(F . n1),(F . (n1 - 1))] in the InternalRel of R or [(F . (n1 - 1)),(F . n1)] in the InternalRel of R )
len p1 < (len p1) + 1 by XREAL_1:29;
then A45: len p1 < n1 by A44, XXREAL_0:2;
then reconsider k = n1 - (len p1) as Element of NAT by INT_1:3, XREAL_1:48;
((len p1) + 1) - 1 < n1 - 1 by A44, XREAL_1:9;
then F . n11 = p2 . (n11 - (len p1)) by A41, FINSEQ_1:24;
then A46: F . (n1 - 1) = p2 . (k - 1) ;
1 < n1 - (len p1) by A44, XREAL_1:20;
then A47: 1 + 1 <= n1 - (len p1) by INT_1:7;
n1 <= (len p1) + (len p2) by A37, FINSEQ_1:22;
then A48: k <= len p2 by XREAL_1:20;
F . n1 = p2 . k by A37, A45, FINSEQ_1:24;
hence ( [(F . n1),(F . (n1 - 1))] in the InternalRel of R or [(F . (n1 - 1)),(F . n1)] in the InternalRel of R ) by A34, A46, A47, A48; ::_thesis: verum
end;
supposeA49: (len p1) + 1 = n1 ; ::_thesis: ( [(F . n1),(F . (n1 - 1))] in the InternalRel of R or [(F . (n1 - 1)),(F . n1)] in the InternalRel of R )
( (len p1) + 1 <= (len p1) + (len p2) & ((len p1) + 1) - (len p1) = 1 ) by A31, XREAL_1:8;
then A50: F . n1 = y by A32, A49, FINSEQ_1:23;
len p1 in dom p1 by A27, FINSEQ_3:25;
then F . (n1 - 1) = y by A29, A49, FINSEQ_1:def_7;
hence ( [(F . n1),(F . (n1 - 1))] in the InternalRel of R or [(F . (n1 - 1)),(F . n1)] in the InternalRel of R ) by A18, A24, A50, RELAT_2:def_1; ::_thesis: verum
end;
end;
end;
hence [x,z] in P1 by A23, A25; ::_thesis: verum
end;
then P1 is_transitive_in the carrier of R by RELAT_2:def_8;
then reconsider P1 = { [x,y] where x, y is Element of R : ( x in the carrier of R & y in the carrier of R & S1[x,y] ) } as Equivalence_Relation of the carrier of R by A22, A17, PARTFUN1:def_2, RELAT_2:def_11, RELAT_2:def_16;
take P1 ; ::_thesis: for x, y being set holds
( [x,y] in P1 iff ( x in the carrier of R & y in the carrier of R & ex p being FinSequence of the carrier of R st
( 1 < len p & p . 1 = x & p . (len p) = y & ( for n being Nat st 2 <= n & n <= len p & not [(p . n),(p . (n - 1))] in the InternalRel of R holds
[(p . (n - 1)),(p . n)] in the InternalRel of R ) ) ) )
thus for x, y being set holds
( [x,y] in P1 iff ( x in the carrier of R & y in the carrier of R & ex p being FinSequence of the carrier of R st
( 1 < len p & p . 1 = x & p . (len p) = y & ( for n being Nat st 2 <= n & n <= len p & not [(p . n),(p . (n - 1))] in the InternalRel of R holds
[(p . (n - 1)),(p . n)] in the InternalRel of R ) ) ) ) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being Equivalence_Relation of the carrier of R st ( for x, y being set holds
( [x,y] in b1 iff ( x in the carrier of R & y in the carrier of R & ex p being FinSequence of the carrier of R st
( 1 < len p & p . 1 = x & p . (len p) = y & ( for n being Nat st 2 <= n & n <= len p & not [(p . n),(p . (n - 1))] in the InternalRel of R holds
[(p . (n - 1)),(p . n)] in the InternalRel of R ) ) ) ) ) & ( for x, y being set holds
( [x,y] in b2 iff ( x in the carrier of R & y in the carrier of R & ex p being FinSequence of the carrier of R st
( 1 < len p & p . 1 = x & p . (len p) = y & ( for n being Nat st 2 <= n & n <= len p & not [(p . n),(p . (n - 1))] in the InternalRel of R holds
[(p . (n - 1)),(p . n)] in the InternalRel of R ) ) ) ) ) holds
b1 = b2
proof
let X, Y be Equivalence_Relation of the carrier of R; ::_thesis: ( ( for x, y being set holds
( [x,y] in X iff ( x in the carrier of R & y in the carrier of R & ex p being FinSequence of the carrier of R st
( 1 < len p & p . 1 = x & p . (len p) = y & ( for n being Nat st 2 <= n & n <= len p & not [(p . n),(p . (n - 1))] in the InternalRel of R holds
[(p . (n - 1)),(p . n)] in the InternalRel of R ) ) ) ) ) & ( for x, y being set holds
( [x,y] in Y iff ( x in the carrier of R & y in the carrier of R & ex p being FinSequence of the carrier of R st
( 1 < len p & p . 1 = x & p . (len p) = y & ( for n being Nat st 2 <= n & n <= len p & not [(p . n),(p . (n - 1))] in the InternalRel of R holds
[(p . (n - 1)),(p . n)] in the InternalRel of R ) ) ) ) ) implies X = Y )
defpred S1[ set , set ] means ( $1 in the carrier of R & $2 in the carrier of R & ex p being FinSequence of the carrier of R st
( 1 < len p & p . 1 = $1 & p . (len p) = $2 & ( for n being Nat st 2 <= n & n <= len p & not [(p . n),(p . (n - 1))] in the InternalRel of R holds
[(p . (n - 1)),(p . n)] in the InternalRel of R ) ) );
assume A51: for x, y being set holds
( [x,y] in X iff S1[x,y] ) ; ::_thesis: ( ex x, y being set st
( ( [x,y] in Y implies ( x in the carrier of R & y in the carrier of R & ex p being FinSequence of the carrier of R st
( 1 < len p & p . 1 = x & p . (len p) = y & ( for n being Nat st 2 <= n & n <= len p & not [(p . n),(p . (n - 1))] in the InternalRel of R holds
[(p . (n - 1)),(p . n)] in the InternalRel of R ) ) ) ) implies ( x in the carrier of R & y in the carrier of R & ex p being FinSequence of the carrier of R st
( 1 < len p & p . 1 = x & p . (len p) = y & ( for n being Nat st 2 <= n & n <= len p & not [(p . n),(p . (n - 1))] in the InternalRel of R holds
[(p . (n - 1)),(p . n)] in the InternalRel of R ) ) & not [x,y] in Y ) ) or X = Y )
assume A52: for x, y being set holds
( [x,y] in Y iff S1[x,y] ) ; ::_thesis: X = Y
for x, y being set holds
( [x,y] in X iff [x,y] in Y )
proof
let x, y be set ; ::_thesis: ( [x,y] in X iff [x,y] in Y )
hereby ::_thesis: ( [x,y] in Y implies [x,y] in X )
assume [x,y] in X ; ::_thesis: [x,y] in Y
then S1[x,y] by A51;
hence [x,y] in Y by A52; ::_thesis: verum
end;
assume [x,y] in Y ; ::_thesis: [x,y] in X
then S1[x,y] by A52;
hence [x,y] in X by A51; ::_thesis: verum
end;
hence X = Y by RELAT_1:def_2; ::_thesis: verum
end;
end;
:: deftheorem Def3 defines Path_Rel OSALG_4:def_3_:_
for R being non empty Poset
for b2 being Equivalence_Relation of the carrier of R holds
( b2 = Path_Rel R iff for x, y being set holds
( [x,y] in b2 iff ( x in the carrier of R & y in the carrier of R & ex p being FinSequence of the carrier of R st
( 1 < len p & p . 1 = x & p . (len p) = y & ( for n being Nat st 2 <= n & n <= len p & not [(p . n),(p . (n - 1))] in the InternalRel of R holds
[(p . (n - 1)),(p . n)] in the InternalRel of R ) ) ) ) );
theorem Th2: :: OSALG_4:2
for R being non empty Poset
for s1, s2 being Element of R st s1 <= s2 holds
[s1,s2] in Path_Rel R
proof
let R be non empty Poset; ::_thesis: for s1, s2 being Element of R st s1 <= s2 holds
[s1,s2] in Path_Rel R
let s1, s2 be Element of R; ::_thesis: ( s1 <= s2 implies [s1,s2] in Path_Rel R )
assume A1: s1 <= s2 ; ::_thesis: [s1,s2] in Path_Rel R
set p = <*s1,s2*>;
A2: len <*s1,s2*> = 2 by FINSEQ_1:44;
A3: <*s1,s2*> . 1 = s1 by FINSEQ_1:44;
A4: for n being Nat st 2 <= n & n <= len <*s1,s2*> & not [(<*s1,s2*> . n),(<*s1,s2*> . (n - 1))] in the InternalRel of R holds
[(<*s1,s2*> . (n - 1)),(<*s1,s2*> . n)] in the InternalRel of R
proof
let n1 be Nat; ::_thesis: ( 2 <= n1 & n1 <= len <*s1,s2*> & not [(<*s1,s2*> . n1),(<*s1,s2*> . (n1 - 1))] in the InternalRel of R implies [(<*s1,s2*> . (n1 - 1)),(<*s1,s2*> . n1)] in the InternalRel of R )
assume ( 2 <= n1 & n1 <= len <*s1,s2*> ) ; ::_thesis: ( [(<*s1,s2*> . n1),(<*s1,s2*> . (n1 - 1))] in the InternalRel of R or [(<*s1,s2*> . (n1 - 1)),(<*s1,s2*> . n1)] in the InternalRel of R )
then A5: n1 = 2 by A2, XXREAL_0:1;
[s1,s2] in the InternalRel of R by A1, ORDERS_2:def_5;
hence ( [(<*s1,s2*> . n1),(<*s1,s2*> . (n1 - 1))] in the InternalRel of R or [(<*s1,s2*> . (n1 - 1)),(<*s1,s2*> . n1)] in the InternalRel of R ) by A3, A5, FINSEQ_1:44; ::_thesis: verum
end;
<*s1,s2*> . (len <*s1,s2*>) = s2 by A2, FINSEQ_1:44;
hence [s1,s2] in Path_Rel R by A2, A3, A4, Def3; ::_thesis: verum
end;
definition
let R be non empty Poset;
let s1, s2 be Element of R;
preds1 ~= s2 means :Def4: :: OSALG_4:def 4
[s1,s2] in Path_Rel R;
reflexivity
for s1 being Element of R holds [s1,s1] in Path_Rel R
proof
set PR = Path_Rel R;
field (Path_Rel R) = the carrier of R by ORDERS_1:12;
then Path_Rel R is_reflexive_in the carrier of R by RELAT_2:def_9;
hence for s1 being Element of R holds [s1,s1] in Path_Rel R by RELAT_2:def_1; ::_thesis: verum
end;
symmetry
for s1, s2 being Element of R st [s1,s2] in Path_Rel R holds
[s2,s1] in Path_Rel R
proof
set PR = Path_Rel R;
field (Path_Rel R) = the carrier of R by ORDERS_1:12;
then Path_Rel R is_symmetric_in the carrier of R by RELAT_2:def_11;
hence for s1, s2 being Element of R st [s1,s2] in Path_Rel R holds
[s2,s1] in Path_Rel R by RELAT_2:def_3; ::_thesis: verum
end;
end;
:: deftheorem Def4 defines ~= OSALG_4:def_4_:_
for R being non empty Poset
for s1, s2 being Element of R holds
( s1 ~= s2 iff [s1,s2] in Path_Rel R );
theorem :: OSALG_4:3
for R being non empty Poset
for s1, s2, s3 being Element of R st s1 ~= s2 & s2 ~= s3 holds
s1 ~= s3
proof
let R be non empty Poset; ::_thesis: for s1, s2, s3 being Element of R st s1 ~= s2 & s2 ~= s3 holds
s1 ~= s3
let s1, s2, s3 be Element of R; ::_thesis: ( s1 ~= s2 & s2 ~= s3 implies s1 ~= s3 )
set PR = Path_Rel R;
field (Path_Rel R) = the carrier of R by ORDERS_1:12;
then A1: Path_Rel R is_transitive_in the carrier of R by RELAT_2:def_16;
assume ( s1 ~= s2 & s2 ~= s3 ) ; ::_thesis: s1 ~= s3
then ( [s1,s2] in Path_Rel R & [s2,s3] in Path_Rel R ) by Def4;
then [s1,s3] in Path_Rel R by A1, RELAT_2:def_8;
hence s1 ~= s3 by Def4; ::_thesis: verum
end;
definition
let R be non empty Poset;
func Components R -> non empty Subset-Family of R equals :: OSALG_4:def 5
Class (Path_Rel R);
coherence
Class (Path_Rel R) is non empty Subset-Family of R ;
end;
:: deftheorem defines Components OSALG_4:def_5_:_
for R being non empty Poset holds Components R = Class (Path_Rel R);
registration
let R be non empty Poset;
cluster -> non empty for Element of Components R;
coherence
for b1 being Element of Components R holds not b1 is empty
proof
let X be Element of Components R; ::_thesis: not X is empty
ex x being set st
( x in the carrier of R & X = Class ((Path_Rel R),x) ) by EQREL_1:def_3;
hence not X is empty by EQREL_1:20; ::_thesis: verum
end;
end;
definition
let R be non empty Poset;
mode Component of R is Element of Components R;
end;
definition
let R be non empty Poset;
let s1 be Element of R;
func CComp s1 -> Component of R equals :: OSALG_4:def 6
Class ((Path_Rel R),s1);
correctness
coherence
Class ((Path_Rel R),s1) is Component of R;
by EQREL_1:def_3;
end;
:: deftheorem defines CComp OSALG_4:def_6_:_
for R being non empty Poset
for s1 being Element of R holds CComp s1 = Class ((Path_Rel R),s1);
theorem Th4: :: OSALG_4:4
for R being non empty Poset
for s1, s2 being Element of R st s1 <= s2 holds
CComp s1 = CComp s2
proof
let R be non empty Poset; ::_thesis: for s1, s2 being Element of R st s1 <= s2 holds
CComp s1 = CComp s2
let s1, s2 be Element of R; ::_thesis: ( s1 <= s2 implies CComp s1 = CComp s2 )
assume s1 <= s2 ; ::_thesis: CComp s1 = CComp s2
then [s1,s2] in Path_Rel R by Th2;
hence CComp s1 = CComp s2 by EQREL_1:35; ::_thesis: verum
end;
definition
let R be non empty Poset;
let A be ManySortedSet of the carrier of R;
let C be Component of R;
funcA -carrier_of C -> set equals :: OSALG_4:def 7
union { (A . s) where s is Element of R : s in C } ;
correctness
coherence
union { (A . s) where s is Element of R : s in C } is set ;
;
end;
:: deftheorem defines -carrier_of OSALG_4:def_7_:_
for R being non empty Poset
for A being ManySortedSet of the carrier of R
for C being Component of R holds A -carrier_of C = union { (A . s) where s is Element of R : s in C } ;
theorem Th5: :: OSALG_4:5
for R being non empty Poset
for A being ManySortedSet of the carrier of R
for s being Element of R
for x being set st x in A . s holds
x in A -carrier_of (CComp s)
proof
let R be non empty Poset; ::_thesis: for A being ManySortedSet of the carrier of R
for s being Element of R
for x being set st x in A . s holds
x in A -carrier_of (CComp s)
let A be ManySortedSet of the carrier of R; ::_thesis: for s being Element of R
for x being set st x in A . s holds
x in A -carrier_of (CComp s)
let s be Element of R; ::_thesis: for x being set st x in A . s holds
x in A -carrier_of (CComp s)
let x be set ; ::_thesis: ( x in A . s implies x in A -carrier_of (CComp s) )
assume A1: x in A . s ; ::_thesis: x in A -carrier_of (CComp s)
s in CComp s by EQREL_1:20;
then A . s in { (A . s1) where s1 is Element of R : s1 in CComp s } ;
hence x in A -carrier_of (CComp s) by A1, TARSKI:def_4; ::_thesis: verum
end;
definition
let R be non empty Poset;
attrR is locally_directed means :Def8: :: OSALG_4:def 8
for C being Component of R holds C is directed ;
end;
:: deftheorem Def8 defines locally_directed OSALG_4:def_8_:_
for R being non empty Poset holds
( R is locally_directed iff for C being Component of R holds C is directed );
theorem Th6: :: OSALG_4:6
for R being non empty discrete Poset
for x, y being Element of R st [x,y] in Path_Rel R holds
x = y
proof
let R be non empty discrete Poset; ::_thesis: for x, y being Element of R st [x,y] in Path_Rel R holds
x = y
let x, y be Element of R; ::_thesis: ( [x,y] in Path_Rel R implies x = y )
assume [x,y] in Path_Rel R ; ::_thesis: x = y
then consider p being FinSequence of the carrier of R such that
A1: 1 < len p and
A2: p . 1 = x and
A3: p . (len p) = y and
A4: for n being Nat st 2 <= n & n <= len p & not [(p . n),(p . (n - 1))] in the InternalRel of R holds
[(p . (n - 1)),(p . n)] in the InternalRel of R by Def3;
for n1 being Nat st 1 <= n1 & n1 <= len p holds
p . n1 = x
proof
defpred S1[ Nat] means ( p . $1 <> x & 1 <= $1 );
let n1 be Nat; ::_thesis: ( 1 <= n1 & n1 <= len p implies p . n1 = x )
assume that
A5: 1 <= n1 and
A6: n1 <= len p ; ::_thesis: p . n1 = x
assume A7: p . n1 <> x ; ::_thesis: contradiction
then A8: ex k being Nat st S1[k] by A5;
consider k being Nat such that
A9: ( S1[k] & ( for n being Nat st S1[n] holds
k <= n ) ) from NAT_1:sch_5(A8);
1 < k by A2, A9, XXREAL_0:1;
then A10: 1 + 1 <= k by INT_1:7;
then A11: (1 + 1) - 1 <= k - 1 by XREAL_1:9;
then reconsider k1 = k - 1 as Element of NAT by INT_1:3, XXREAL_0:2;
A12: p . k1 = x by A9, A11, XREAL_1:146;
k <= n1 by A5, A7, A9;
then A13: k <= len p by A6, XXREAL_0:2;
then k in dom p by A9, FINSEQ_3:25;
then reconsider pk = p . k as Element of R by PARTFUN1:4;
percases ( [pk,x] in the InternalRel of R or [x,pk] in the InternalRel of R ) by A4, A10, A13, A12;
suppose [pk,x] in the InternalRel of R ; ::_thesis: contradiction
then pk <= x by ORDERS_2:def_5;
hence contradiction by A9, ORDERS_3:1; ::_thesis: verum
end;
suppose [x,pk] in the InternalRel of R ; ::_thesis: contradiction
then x <= pk by ORDERS_2:def_5;
hence contradiction by A9, ORDERS_3:1; ::_thesis: verum
end;
end;
end;
hence x = y by A1, A3; ::_thesis: verum
end;
theorem Th7: :: OSALG_4:7
for R being non empty discrete Poset
for C being Component of R ex x being Element of R st C = {x}
proof
let R be non empty discrete Poset; ::_thesis: for C being Component of R ex x being Element of R st C = {x}
let C be Component of R; ::_thesis: ex x being Element of R st C = {x}
consider x being set such that
A1: x in the carrier of R and
A2: C = Class ((Path_Rel R),x) by EQREL_1:def_3;
reconsider x1 = x as Element of R by A1;
take x1 ; ::_thesis: C = {x1}
for y being set holds
( y in C iff y = x1 )
proof
let y be set ; ::_thesis: ( y in C iff y = x1 )
hereby ::_thesis: ( y = x1 implies y in C )
assume A3: y in C ; ::_thesis: y = x1
then reconsider y1 = y as Element of R ;
[y,x] in Path_Rel R by A2, A3, EQREL_1:19;
then y1 = x1 by Th6;
hence y = x1 ; ::_thesis: verum
end;
assume y = x1 ; ::_thesis: y in C
hence y in C by A2, EQREL_1:20; ::_thesis: verum
end;
hence C = {x1} by TARSKI:def_1; ::_thesis: verum
end;
theorem Th8: :: OSALG_4:8
for R being non empty discrete Poset holds R is locally_directed
proof
let R be non empty discrete Poset; ::_thesis: R is locally_directed
let C be Component of R; :: according to OSALG_4:def_8 ::_thesis: C is directed
consider x being Element of R such that
A1: C = {x} by Th7;
for x, y being Element of R st x in C & y in C holds
ex z being Element of R st
( z in C & x <= z & y <= z )
proof
let x1, y1 be Element of R; ::_thesis: ( x1 in C & y1 in C implies ex z being Element of R st
( z in C & x1 <= z & y1 <= z ) )
assume that
A2: x1 in C and
A3: y1 in C ; ::_thesis: ex z being Element of R st
( z in C & x1 <= z & y1 <= z )
take x1 ; ::_thesis: ( x1 in C & x1 <= x1 & y1 <= x1 )
x1 = x by A1, A2, TARSKI:def_1;
hence ( x1 in C & x1 <= x1 & y1 <= x1 ) by A1, A3, TARSKI:def_1; ::_thesis: verum
end;
hence C is directed by WAYBEL_0:def_1; ::_thesis: verum
end;
registration
cluster non empty reflexive transitive antisymmetric locally_directed for RelStr ;
existence
ex b1 being non empty Poset st b1 is locally_directed
proof
set R = the non empty discrete Poset;
take the non empty discrete Poset ; ::_thesis: the non empty discrete Poset is locally_directed
thus the non empty discrete Poset is locally_directed by Th8; ::_thesis: verum
end;
end;
registration
cluster non empty non void V73() reflexive transitive antisymmetric order-sorted discernable locally_directed for OverloadedRSSign ;
existence
ex b1 being OrderSortedSign st b1 is locally_directed
proof
set R = the discrete OrderSortedSign;
take the discrete OrderSortedSign ; ::_thesis: the discrete OrderSortedSign is locally_directed
thus the discrete OrderSortedSign is locally_directed by Th8; ::_thesis: verum
end;
end;
registration
cluster non empty reflexive transitive antisymmetric discrete -> non empty locally_directed for RelStr ;
coherence
for b1 being non empty Poset st b1 is discrete holds
b1 is locally_directed by Th8;
end;
registration
let S be non empty locally_directed Poset;
cluster -> directed for Element of Components S;
coherence
for b1 being Component of S holds b1 is directed by Def8;
end;
theorem Th9: :: OSALG_4:9
{} is Equivalence_Relation of {} by RELSET_1:12;
definition
let S be locally_directed OrderSortedSign;
let A be OSAlgebra of S;
let E be MSEquivalence-like OrderSortedRelation of A;
let C be Component of S;
func CompClass (E,C) -> Equivalence_Relation of ( the Sorts of A -carrier_of C) means :Def9: :: OSALG_4:def 9
for x, y being set holds
( [x,y] in it iff ex s1 being Element of S st
( s1 in C & [x,y] in E . s1 ) );
existence
ex b1 being Equivalence_Relation of ( the Sorts of A -carrier_of C) st
for x, y being set holds
( [x,y] in b1 iff ex s1 being Element of S st
( s1 in C & [x,y] in E . s1 ) )
proof
defpred S1[ set , set ] means ex s1 being Element of S st
( s1 in C & [$1,$2] in E . s1 );
A1: E is os-compatible by Def2;
percases ( the Sorts of A -carrier_of C is empty or not the Sorts of A -carrier_of C is empty ) ;
supposeA2: the Sorts of A -carrier_of C is empty ; ::_thesis: ex b1 being Equivalence_Relation of ( the Sorts of A -carrier_of C) st
for x, y being set holds
( [x,y] in b1 iff ex s1 being Element of S st
( s1 in C & [x,y] in E . s1 ) )
for x, y being set holds
( [x,y] in {} iff ex s1 being Element of S st
( s1 in C & [x,y] in E . s1 ) )
proof
let x, y be set ; ::_thesis: ( [x,y] in {} iff ex s1 being Element of S st
( s1 in C & [x,y] in E . s1 ) )
thus ( [x,y] in {} implies ex s1 being Element of S st
( s1 in C & [x,y] in E . s1 ) ) ; ::_thesis: ( ex s1 being Element of S st
( s1 in C & [x,y] in E . s1 ) implies [x,y] in {} )
assume ex s1 being Element of S st
( s1 in C & [x,y] in E . s1 ) ; ::_thesis: [x,y] in {}
then consider s1 being Element of S such that
A3: ( s1 in C & [x,y] in E . s1 ) ;
( x in the Sorts of A . s1 & the Sorts of A . s1 in { ( the Sorts of A . s) where s is Element of S : s in C } ) by A3, ZFMISC_1:87;
hence [x,y] in {} by A2, TARSKI:def_4; ::_thesis: verum
end;
hence ex b1 being Equivalence_Relation of ( the Sorts of A -carrier_of C) st
for x, y being set holds
( [x,y] in b1 iff ex s1 being Element of S st
( s1 in C & [x,y] in E . s1 ) ) by A2, Th9; ::_thesis: verum
end;
suppose not the Sorts of A -carrier_of C is empty ; ::_thesis: ex b1 being Equivalence_Relation of ( the Sorts of A -carrier_of C) st
for x, y being set holds
( [x,y] in b1 iff ex s1 being Element of S st
( s1 in C & [x,y] in E . s1 ) )
then reconsider SAC = the Sorts of A -carrier_of C as non empty set ;
set CC = { [x,y] where x, y is Element of SAC : S1[x,y] } ;
{ [x,y] where x, y is Element of SAC : S1[x,y] } c= [:SAC,SAC:]
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { [x,y] where x, y is Element of SAC : S1[x,y] } or z in [:SAC,SAC:] )
assume z in { [x,y] where x, y is Element of SAC : S1[x,y] } ; ::_thesis: z in [:SAC,SAC:]
then ex x, y being Element of SAC st
( z = [x,y] & S1[x,y] ) ;
hence z in [:SAC,SAC:] by ZFMISC_1:87; ::_thesis: verum
end;
then reconsider P1 = { [x,y] where x, y is Element of SAC : S1[x,y] } as Relation of SAC ;
now__::_thesis:_for_x,_y_being_set_st_x_in_SAC_&_y_in_SAC_&_[x,y]_in_P1_holds_
[y,x]_in_P1
let x, y be set ; ::_thesis: ( x in SAC & y in SAC & [x,y] in P1 implies [y,x] in P1 )
assume that
A4: ( x in SAC & y in SAC ) and
A5: [x,y] in P1 ; ::_thesis: [y,x] in P1
reconsider x1 = x, y1 = y as Element of SAC by A4;
consider x2, y2 being Element of SAC such that
A6: [x,y] = [x2,y2] and
A7: S1[x2,y2] by A5;
A8: ( x = x2 & y = y2 ) by A6, XTUPLE_0:1;
consider s5 being Element of S such that
A9: s5 in C and
A10: [x2,y2] in E . s5 by A7;
field (E . s5) = the Sorts of A . s5 by ORDERS_1:12;
then A11: E . s5 is_symmetric_in the Sorts of A . s5 by RELAT_2:def_11;
( x2 in the Sorts of A . s5 & y2 in the Sorts of A . s5 ) by A10, ZFMISC_1:87;
then [y,x] in E . s5 by A8, A10, A11, RELAT_2:def_3;
then [y1,x1] in { [x,y] where x, y is Element of SAC : S1[x,y] } by A9;
hence [y,x] in P1 ; ::_thesis: verum
end;
then A12: P1 is_symmetric_in SAC by RELAT_2:def_3;
now__::_thesis:_for_x_being_set_st_x_in_SAC_holds_
[x,x]_in_P1
let x be set ; ::_thesis: ( x in SAC implies [x,x] in P1 )
assume A13: x in SAC ; ::_thesis: [x,x] in P1
reconsider x1 = x as Element of SAC by A13;
consider X being set such that
A14: x in X and
A15: X in { ( the Sorts of A . s) where s is Element of S : s in C } by A13, TARSKI:def_4;
consider s being Element of S such that
A16: X = the Sorts of A . s and
A17: s in C by A15;
field (E . s) = the Sorts of A . s by ORDERS_1:12;
then E . s is_reflexive_in the Sorts of A . s by RELAT_2:def_9;
then [x,x] in E . s by A14, A16, RELAT_2:def_1;
then [x1,x1] in { [x,y] where x, y is Element of SAC : S1[x,y] } by A17;
hence [x,x] in P1 ; ::_thesis: verum
end;
then P1 is_reflexive_in SAC by RELAT_2:def_1;
then A18: ( dom P1 = SAC & field P1 = SAC ) by ORDERS_1:13;
now__::_thesis:_for_x,_y,_z_being_set_st_x_in_SAC_&_y_in_SAC_&_z_in_SAC_&_[x,y]_in_P1_&_[y,z]_in_P1_holds_
[x,z]_in_P1
let x, y, z be set ; ::_thesis: ( x in SAC & y in SAC & z in SAC & [x,y] in P1 & [y,z] in P1 implies [x,z] in P1 )
assume that
x in SAC and
y in SAC and
z in SAC and
A19: [x,y] in P1 and
A20: [y,z] in P1 ; ::_thesis: [x,z] in P1
consider x2, y2 being Element of SAC such that
A21: [x,y] = [x2,y2] and
A22: S1[x2,y2] by A19;
A23: x = x2 by A21, XTUPLE_0:1;
consider y3, z3 being Element of SAC such that
A24: [y,z] = [y3,z3] and
A25: S1[y3,z3] by A20;
A26: y = y3 by A24, XTUPLE_0:1;
consider s5 being Element of S such that
A27: s5 in C and
A28: [x2,y2] in E . s5 by A22;
consider s6 being Element of S such that
A29: s6 in C and
A30: [y3,z3] in E . s6 by A25;
reconsider s51 = s5, s61 = s6 as Element of S ;
consider su being Element of S such that
A31: su in C and
A32: s51 <= su and
A33: s61 <= su by A27, A29, WAYBEL_0:def_1;
( y3 in the Sorts of A . s6 & z3 in the Sorts of A . s6 ) by A30, ZFMISC_1:87;
then A34: [y3,z3] in E . su by A1, A30, A33, Def1;
then A35: z3 in the Sorts of A . su by ZFMISC_1:87;
A36: z = z3 by A24, XTUPLE_0:1;
A37: y = y2 by A21, XTUPLE_0:1;
field (E . su) = the Sorts of A . su by ORDERS_1:12;
then A38: E . su is_transitive_in the Sorts of A . su by RELAT_2:def_16;
( x2 in the Sorts of A . s5 & y2 in the Sorts of A . s5 ) by A28, ZFMISC_1:87;
then A39: [x2,y2] in E . su by A1, A28, A32, Def1;
then ( x2 in the Sorts of A . su & y2 in the Sorts of A . su ) by ZFMISC_1:87;
then [x2,z3] in E . su by A37, A26, A39, A34, A35, A38, RELAT_2:def_8;
hence [x,z] in P1 by A23, A36, A31; ::_thesis: verum
end;
then P1 is_transitive_in SAC by RELAT_2:def_8;
then reconsider P1 = P1 as Equivalence_Relation of ( the Sorts of A -carrier_of C) by A18, A12, PARTFUN1:def_2, RELAT_2:def_11, RELAT_2:def_16;
take P1 ; ::_thesis: for x, y being set holds
( [x,y] in P1 iff ex s1 being Element of S st
( s1 in C & [x,y] in E . s1 ) )
for x, y being set holds
( [x,y] in { [x,y] where x, y is Element of SAC : S1[x,y] } iff S1[x,y] )
proof
let x, y be set ; ::_thesis: ( [x,y] in { [x,y] where x, y is Element of SAC : S1[x,y] } iff S1[x,y] )
hereby ::_thesis: ( S1[x,y] implies [x,y] in { [x,y] where x, y is Element of SAC : S1[x,y] } )
assume [x,y] in { [x,y] where x, y is Element of SAC : S1[x,y] } ; ::_thesis: S1[x,y]
then ex x1, y1 being Element of SAC st
( [x,y] = [x1,y1] & S1[x1,y1] ) ;
hence S1[x,y] ; ::_thesis: verum
end;
assume A40: S1[x,y] ; ::_thesis: [x,y] in { [x,y] where x, y is Element of SAC : S1[x,y] }
then consider s1 being Element of S such that
A41: s1 in C and
A42: [x,y] in E . s1 ;
A43: y in the Sorts of A . s1 by A42, ZFMISC_1:87;
( the Sorts of A . s1 in { ( the Sorts of A . s) where s is Element of S : s in C } & x in the Sorts of A . s1 ) by A41, A42, ZFMISC_1:87;
then reconsider x1 = x, y1 = y as Element of SAC by A43, TARSKI:def_4;
[x1,y1] in { [x,y] where x, y is Element of SAC : S1[x,y] } by A40;
hence [x,y] in { [x,y] where x, y is Element of SAC : S1[x,y] } ; ::_thesis: verum
end;
hence for x, y being set holds
( [x,y] in P1 iff ex s1 being Element of S st
( s1 in C & [x,y] in E . s1 ) ) ; ::_thesis: verum
end;
end;
end;
uniqueness
for b1, b2 being Equivalence_Relation of ( the Sorts of A -carrier_of C) st ( for x, y being set holds
( [x,y] in b1 iff ex s1 being Element of S st
( s1 in C & [x,y] in E . s1 ) ) ) & ( for x, y being set holds
( [x,y] in b2 iff ex s1 being Element of S st
( s1 in C & [x,y] in E . s1 ) ) ) holds
b1 = b2
proof
let X, Y be Equivalence_Relation of ( the Sorts of A -carrier_of C); ::_thesis: ( ( for x, y being set holds
( [x,y] in X iff ex s1 being Element of S st
( s1 in C & [x,y] in E . s1 ) ) ) & ( for x, y being set holds
( [x,y] in Y iff ex s1 being Element of S st
( s1 in C & [x,y] in E . s1 ) ) ) implies X = Y )
defpred S1[ set , set ] means ex s1 being Element of S st
( s1 in C & [$1,$2] in E . s1 );
assume A44: for x, y being set holds
( [x,y] in X iff S1[x,y] ) ; ::_thesis: ( ex x, y being set st
( ( [x,y] in Y implies ex s1 being Element of S st
( s1 in C & [x,y] in E . s1 ) ) implies ( ex s1 being Element of S st
( s1 in C & [x,y] in E . s1 ) & not [x,y] in Y ) ) or X = Y )
assume A45: for x, y being set holds
( [x,y] in Y iff S1[x,y] ) ; ::_thesis: X = Y
for x, y being set holds
( [x,y] in X iff [x,y] in Y )
proof
let x, y be set ; ::_thesis: ( [x,y] in X iff [x,y] in Y )
hereby ::_thesis: ( [x,y] in Y implies [x,y] in X )
assume [x,y] in X ; ::_thesis: [x,y] in Y
then S1[x,y] by A44;
hence [x,y] in Y by A45; ::_thesis: verum
end;
assume [x,y] in Y ; ::_thesis: [x,y] in X
then S1[x,y] by A45;
hence [x,y] in X by A44; ::_thesis: verum
end;
hence X = Y by RELAT_1:def_2; ::_thesis: verum
end;
end;
:: deftheorem Def9 defines CompClass OSALG_4:def_9_:_
for S being locally_directed OrderSortedSign
for A being OSAlgebra of S
for E being MSEquivalence-like OrderSortedRelation of A
for C being Component of S
for b5 being Equivalence_Relation of ( the Sorts of A -carrier_of C) holds
( b5 = CompClass (E,C) iff for x, y being set holds
( [x,y] in b5 iff ex s1 being Element of S st
( s1 in C & [x,y] in E . s1 ) ) );
definition
let S be locally_directed OrderSortedSign;
let A be OSAlgebra of S;
let E be MSEquivalence-like OrderSortedRelation of A;
let s1 be Element of S;
func OSClass (E,s1) -> Subset of (Class (CompClass (E,(CComp s1)))) means :Def10: :: OSALG_4:def 10
for z being set holds
( z in it iff ex x being set st
( x in the Sorts of A . s1 & z = Class ((CompClass (E,(CComp s1))),x) ) );
existence
ex b1 being Subset of (Class (CompClass (E,(CComp s1)))) st
for z being set holds
( z in b1 iff ex x being set st
( x in the Sorts of A . s1 & z = Class ((CompClass (E,(CComp s1))),x) ) )
proof
set SAC = the Sorts of A -carrier_of (CComp s1);
set CS = Class (CompClass (E,(CComp s1)));
defpred S1[ set ] means ex x being set st
( x in the Sorts of A . s1 & $1 = Class ((CompClass (E,(CComp s1))),x) );
percases ( Class (CompClass (E,(CComp s1))) is empty or not Class (CompClass (E,(CComp s1))) is empty ) ;
supposeA1: Class (CompClass (E,(CComp s1))) is empty ; ::_thesis: ex b1 being Subset of (Class (CompClass (E,(CComp s1)))) st
for z being set holds
( z in b1 iff ex x being set st
( x in the Sorts of A . s1 & z = Class ((CompClass (E,(CComp s1))),x) ) )
reconsider CS1 = {} as Subset of (Class (CompClass (E,(CComp s1)))) by XBOOLE_1:2;
take CS1 ; ::_thesis: for z being set holds
( z in CS1 iff ex x being set st
( x in the Sorts of A . s1 & z = Class ((CompClass (E,(CComp s1))),x) ) )
let z be set ; ::_thesis: ( z in CS1 iff ex x being set st
( x in the Sorts of A . s1 & z = Class ((CompClass (E,(CComp s1))),x) ) )
thus ( z in CS1 implies S1[z] ) ; ::_thesis: ( ex x being set st
( x in the Sorts of A . s1 & z = Class ((CompClass (E,(CComp s1))),x) ) implies z in CS1 )
assume S1[z] ; ::_thesis: z in CS1
then consider x being set such that
A2: x in the Sorts of A . s1 and
z = Class ((CompClass (E,(CComp s1))),x) ;
x in the Sorts of A -carrier_of (CComp s1) by A2, Th5;
hence z in CS1 by A1; ::_thesis: verum
end;
suppose not Class (CompClass (E,(CComp s1))) is empty ; ::_thesis: ex b1 being Subset of (Class (CompClass (E,(CComp s1)))) st
for z being set holds
( z in b1 iff ex x being set st
( x in the Sorts of A . s1 & z = Class ((CompClass (E,(CComp s1))),x) ) )
then reconsider CS1 = Class (CompClass (E,(CComp s1))) as non empty Subset-Family of ( the Sorts of A -carrier_of (CComp s1)) ;
set CC = { x where x is Element of CS1 : S1[x] } ;
now__::_thesis:_for_x_being_set_st_x_in__{__x_where_x_is_Element_of_CS1_:_S1[x]__}__holds_
x_in_CS1
let x be set ; ::_thesis: ( x in { x where x is Element of CS1 : S1[x] } implies x in CS1 )
assume x in { x where x is Element of CS1 : S1[x] } ; ::_thesis: x in CS1
then ex y being Element of CS1 st
( x = y & S1[y] ) ;
hence x in CS1 ; ::_thesis: verum
end;
then reconsider CC2 = { x where x is Element of CS1 : S1[x] } as Subset of (Class (CompClass (E,(CComp s1)))) by TARSKI:def_3;
take CC2 ; ::_thesis: for z being set holds
( z in CC2 iff ex x being set st
( x in the Sorts of A . s1 & z = Class ((CompClass (E,(CComp s1))),x) ) )
for x being set holds
( x in { x where x is Element of CS1 : S1[x] } iff S1[x] )
proof
let x be set ; ::_thesis: ( x in { x where x is Element of CS1 : S1[x] } iff S1[x] )
hereby ::_thesis: ( S1[x] implies x in { x where x is Element of CS1 : S1[x] } )
assume x in { x where x is Element of CS1 : S1[x] } ; ::_thesis: S1[x]
then ex x1 being Element of CS1 st
( x = x1 & S1[x1] ) ;
hence S1[x] ; ::_thesis: verum
end;
assume A3: S1[x] ; ::_thesis: x in { x where x is Element of CS1 : S1[x] }
then consider y being set such that
A4: y in the Sorts of A . s1 and
A5: x = Class ((CompClass (E,(CComp s1))),y) ;
s1 in CComp s1 by EQREL_1:20;
then the Sorts of A . s1 in { ( the Sorts of A . s) where s is Element of S : s in CComp s1 } ;
then y in union { ( the Sorts of A . s) where s is Element of S : s in CComp s1 } by A4, TARSKI:def_4;
then x in Class (CompClass (E,(CComp s1))) by A5, EQREL_1:def_3;
hence x in { x where x is Element of CS1 : S1[x] } by A3; ::_thesis: verum
end;
hence for z being set holds
( z in CC2 iff ex x being set st
( x in the Sorts of A . s1 & z = Class ((CompClass (E,(CComp s1))),x) ) ) ; ::_thesis: verum
end;
end;
end;
uniqueness
for b1, b2 being Subset of (Class (CompClass (E,(CComp s1)))) st ( for z being set holds
( z in b1 iff ex x being set st
( x in the Sorts of A . s1 & z = Class ((CompClass (E,(CComp s1))),x) ) ) ) & ( for z being set holds
( z in b2 iff ex x being set st
( x in the Sorts of A . s1 & z = Class ((CompClass (E,(CComp s1))),x) ) ) ) holds
b1 = b2
proof
let X, Y be Subset of (Class (CompClass (E,(CComp s1)))); ::_thesis: ( ( for z being set holds
( z in X iff ex x being set st
( x in the Sorts of A . s1 & z = Class ((CompClass (E,(CComp s1))),x) ) ) ) & ( for z being set holds
( z in Y iff ex x being set st
( x in the Sorts of A . s1 & z = Class ((CompClass (E,(CComp s1))),x) ) ) ) implies X = Y )
defpred S1[ set ] means ex x being set st
( x in the Sorts of A . s1 & $1 = Class ((CompClass (E,(CComp s1))),x) );
assume A6: for x being set holds
( x in X iff S1[x] ) ; ::_thesis: ( ex z being set st
( ( z in Y implies ex x being set st
( x in the Sorts of A . s1 & z = Class ((CompClass (E,(CComp s1))),x) ) ) implies ( ex x being set st
( x in the Sorts of A . s1 & z = Class ((CompClass (E,(CComp s1))),x) ) & not z in Y ) ) or X = Y )
assume A7: for x being set holds
( x in Y iff S1[x] ) ; ::_thesis: X = Y
for x being set holds
( x in X iff x in Y )
proof
let x be set ; ::_thesis: ( x in X iff x in Y )
hereby ::_thesis: ( x in Y implies x in X )
assume x in X ; ::_thesis: x in Y
then S1[x] by A6;
hence x in Y by A7; ::_thesis: verum
end;
assume x in Y ; ::_thesis: x in X
then S1[x] by A7;
hence x in X by A6; ::_thesis: verum
end;
hence X = Y by TARSKI:1; ::_thesis: verum
end;
end;
:: deftheorem Def10 defines OSClass OSALG_4:def_10_:_
for S being locally_directed OrderSortedSign
for A being OSAlgebra of S
for E being MSEquivalence-like OrderSortedRelation of A
for s1 being Element of S
for b5 being Subset of (Class (CompClass (E,(CComp s1)))) holds
( b5 = OSClass (E,s1) iff for z being set holds
( z in b5 iff ex x being set st
( x in the Sorts of A . s1 & z = Class ((CompClass (E,(CComp s1))),x) ) ) );
registration
let S be locally_directed OrderSortedSign;
let A be non-empty OSAlgebra of S;
let E be MSEquivalence-like OrderSortedRelation of A;
let s1 be Element of S;
cluster OSClass (E,s1) -> non empty ;
coherence
not OSClass (E,s1) is empty
proof
consider x being set such that
A1: x in the Sorts of A . s1 by XBOOLE_0:def_1;
Class ((CompClass (E,(CComp s1))),x) in OSClass (E,s1) by A1, Def10;
hence not OSClass (E,s1) is empty ; ::_thesis: verum
end;
end;
theorem Th10: :: OSALG_4:10
for S being locally_directed OrderSortedSign
for A being OSAlgebra of S
for E being MSEquivalence-like OrderSortedRelation of A
for s1, s2 being Element of S st s1 <= s2 holds
OSClass (E,s1) c= OSClass (E,s2)
proof
let S be locally_directed OrderSortedSign; ::_thesis: for A being OSAlgebra of S
for E being MSEquivalence-like OrderSortedRelation of A
for s1, s2 being Element of S st s1 <= s2 holds
OSClass (E,s1) c= OSClass (E,s2)
let A be OSAlgebra of S; ::_thesis: for E being MSEquivalence-like OrderSortedRelation of A
for s1, s2 being Element of S st s1 <= s2 holds
OSClass (E,s1) c= OSClass (E,s2)
let E be MSEquivalence-like OrderSortedRelation of A; ::_thesis: for s1, s2 being Element of S st s1 <= s2 holds
OSClass (E,s1) c= OSClass (E,s2)
let s1, s2 be Element of S; ::_thesis: ( s1 <= s2 implies OSClass (E,s1) c= OSClass (E,s2) )
reconsider s3 = s1, s4 = s2 as Element of S ;
assume A1: s1 <= s2 ; ::_thesis: OSClass (E,s1) c= OSClass (E,s2)
then A2: CComp s1 = CComp s2 by Th4;
thus OSClass (E,s1) c= OSClass (E,s2) ::_thesis: verum
proof
reconsider SO = the Sorts of A as OrderSortedSet of S by OSALG_1:17;
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in OSClass (E,s1) or z in OSClass (E,s2) )
assume z in OSClass (E,s1) ; ::_thesis: z in OSClass (E,s2)
then A3: ex x being set st
( x in the Sorts of A . s1 & z = Class ((CompClass (E,(CComp s1))),x) ) by Def10;
SO . s3 c= SO . s4 by A1, OSALG_1:def_16;
hence z in OSClass (E,s2) by A2, A3, Def10; ::_thesis: verum
end;
end;
definition
let S be locally_directed OrderSortedSign;
let A be OSAlgebra of S;
let E be MSEquivalence-like OrderSortedRelation of A;
func OSClass E -> OrderSortedSet of S means :Def11: :: OSALG_4:def 11
for s1 being Element of S holds it . s1 = OSClass (E,s1);
existence
ex b1 being OrderSortedSet of S st
for s1 being Element of S holds b1 . s1 = OSClass (E,s1)
proof
deffunc H1( Element of S) -> Subset of (Class (CompClass (E,(CComp $1)))) = OSClass (E,$1);
consider f being Function such that
A1: dom f = the carrier of S and
A2: for i being Element of S holds f . i = H1(i) from FUNCT_1:sch_4();
reconsider f1 = f as ManySortedSet of the carrier of S by A1, PARTFUN1:def_2, RELAT_1:def_18;
set f2 = f1;
f1 is order-sorted
proof
let s1, s2 be Element of S; :: according to OSALG_1:def_16 ::_thesis: ( not s1 <= s2 or f1 . s1 c= f1 . s2 )
assume A3: s1 <= s2 ; ::_thesis: f1 . s1 c= f1 . s2
( f1 . s1 = OSClass (E,s1) & f1 . s2 = OSClass (E,s2) ) by A2;
hence f1 . s1 c= f1 . s2 by A3, Th10; ::_thesis: verum
end;
hence ex b1 being OrderSortedSet of S st
for s1 being Element of S holds b1 . s1 = OSClass (E,s1) by A2; ::_thesis: verum
end;
uniqueness
for b1, b2 being OrderSortedSet of S st ( for s1 being Element of S holds b1 . s1 = OSClass (E,s1) ) & ( for s1 being Element of S holds b2 . s1 = OSClass (E,s1) ) holds
b1 = b2
proof
let X, Y be OrderSortedSet of S; ::_thesis: ( ( for s1 being Element of S holds X . s1 = OSClass (E,s1) ) & ( for s1 being Element of S holds Y . s1 = OSClass (E,s1) ) implies X = Y )
assume A4: for s1 being Element of S holds X . s1 = OSClass (E,s1) ; ::_thesis: ( ex s1 being Element of S st not Y . s1 = OSClass (E,s1) or X = Y )
assume A5: for s1 being Element of S holds Y . s1 = OSClass (E,s1) ; ::_thesis: X = Y
now__::_thesis:_for_s1_being_set_st_s1_in_the_carrier_of_S_holds_
X_._s1_=_Y_._s1
let s1 be set ; ::_thesis: ( s1 in the carrier of S implies X . s1 = Y . s1 )
assume s1 in the carrier of S ; ::_thesis: X . s1 = Y . s1
then reconsider s2 = s1 as Element of S ;
thus X . s1 = OSClass (E,s2) by A4
.= Y . s1 by A5 ; ::_thesis: verum
end;
hence X = Y by PBOOLE:3; ::_thesis: verum
end;
end;
:: deftheorem Def11 defines OSClass OSALG_4:def_11_:_
for S being locally_directed OrderSortedSign
for A being OSAlgebra of S
for E being MSEquivalence-like OrderSortedRelation of A
for b4 being OrderSortedSet of S holds
( b4 = OSClass E iff for s1 being Element of S holds b4 . s1 = OSClass (E,s1) );
registration
let S be locally_directed OrderSortedSign;
let A be non-empty OSAlgebra of S;
let E be MSEquivalence-like OrderSortedRelation of A;
cluster OSClass E -> V17() ;
coherence
OSClass E is non-empty
proof
for i being set st i in the carrier of S holds
not (OSClass E) . i is empty
proof
let i be set ; ::_thesis: ( i in the carrier of S implies not (OSClass E) . i is empty )
assume i in the carrier of S ; ::_thesis: not (OSClass E) . i is empty
then reconsider s = i as Element of S ;
(OSClass E) . s = OSClass (E,s) by Def11;
hence not (OSClass E) . i is empty ; ::_thesis: verum
end;
hence OSClass E is non-empty by PBOOLE:def_13; ::_thesis: verum
end;
end;
definition
let S be locally_directed OrderSortedSign;
let U1 be non-empty OSAlgebra of S;
let E be MSEquivalence-like OrderSortedRelation of U1;
let s be Element of S;
let x be Element of the Sorts of U1 . s;
func OSClass (E,x) -> Element of OSClass (E,s) equals :: OSALG_4:def 12
Class ((CompClass (E,(CComp s))),x);
correctness
coherence
Class ((CompClass (E,(CComp s))),x) is Element of OSClass (E,s);
by Def10;
end;
:: deftheorem defines OSClass OSALG_4:def_12_:_
for S being locally_directed OrderSortedSign
for U1 being non-empty OSAlgebra of S
for E being MSEquivalence-like OrderSortedRelation of U1
for s being Element of S
for x being Element of the Sorts of U1 . s holds OSClass (E,x) = Class ((CompClass (E,(CComp s))),x);
theorem :: OSALG_4:11
for R being non empty locally_directed Poset
for x, y being Element of R st ex z being Element of R st
( z <= x & z <= y ) holds
ex u being Element of R st
( x <= u & y <= u )
proof
let R be non empty locally_directed Poset; ::_thesis: for x, y being Element of R st ex z being Element of R st
( z <= x & z <= y ) holds
ex u being Element of R st
( x <= u & y <= u )
let x, y be Element of R; ::_thesis: ( ex z being Element of R st
( z <= x & z <= y ) implies ex u being Element of R st
( x <= u & y <= u ) )
assume ex z being Element of R st
( z <= x & z <= y ) ; ::_thesis: ex u being Element of R st
( x <= u & y <= u )
then consider z being Element of R such that
A1: z <= x and
A2: z <= y ;
reconsider x1 = x, y1 = y as Element of R ;
CComp z = CComp y by A2, Th4;
then A3: y in CComp z by EQREL_1:20;
CComp z = CComp x by A1, Th4;
then x in CComp z by EQREL_1:20;
then ex u being Element of R st
( u in CComp z & x1 <= u & y1 <= u ) by A3, WAYBEL_0:def_1;
hence ex u being Element of R st
( x <= u & y <= u ) ; ::_thesis: verum
end;
theorem Th12: :: OSALG_4:12
for S being locally_directed OrderSortedSign
for U1 being non-empty OSAlgebra of S
for E being MSEquivalence-like OrderSortedRelation of U1
for s being Element of S
for x, y being Element of the Sorts of U1 . s holds
( OSClass (E,x) = OSClass (E,y) iff [x,y] in E . s )
proof
let S be locally_directed OrderSortedSign; ::_thesis: for U1 being non-empty OSAlgebra of S
for E being MSEquivalence-like OrderSortedRelation of U1
for s being Element of S
for x, y being Element of the Sorts of U1 . s holds
( OSClass (E,x) = OSClass (E,y) iff [x,y] in E . s )
let U1 be non-empty OSAlgebra of S; ::_thesis: for E being MSEquivalence-like OrderSortedRelation of U1
for s being Element of S
for x, y being Element of the Sorts of U1 . s holds
( OSClass (E,x) = OSClass (E,y) iff [x,y] in E . s )
let E be MSEquivalence-like OrderSortedRelation of U1; ::_thesis: for s being Element of S
for x, y being Element of the Sorts of U1 . s holds
( OSClass (E,x) = OSClass (E,y) iff [x,y] in E . s )
let s be Element of S; ::_thesis: for x, y being Element of the Sorts of U1 . s holds
( OSClass (E,x) = OSClass (E,y) iff [x,y] in E . s )
let x, y be Element of the Sorts of U1 . s; ::_thesis: ( OSClass (E,x) = OSClass (E,y) iff [x,y] in E . s )
reconsider SU = the Sorts of U1 as OrderSortedSet of S by OSALG_1:17;
A1: s in CComp s by EQREL_1:20;
A2: E is os-compatible by Def2;
A3: x in the Sorts of U1 -carrier_of (CComp s) by Th5;
hereby ::_thesis: ( [x,y] in E . s implies OSClass (E,x) = OSClass (E,y) )
assume OSClass (E,x) = OSClass (E,y) ; ::_thesis: [x,y] in E . s
then [x,y] in CompClass (E,(CComp s)) by A3, EQREL_1:35;
then consider s1 being Element of S such that
A4: s1 in CComp s and
A5: [x,y] in E . s1 by Def9;
reconsider sn1 = s, s11 = s1 as Element of S ;
consider s2 being Element of S such that
s2 in CComp s and
A6: s11 <= s2 and
A7: sn1 <= s2 by A1, A4, WAYBEL_0:def_1;
( x in SU . s11 & y in SU . s11 ) by A5, ZFMISC_1:87;
then [x,y] in E . s2 by A2, A5, A6, Def1;
hence [x,y] in E . s by A2, A7, Def1; ::_thesis: verum
end;
A8: s in CComp s by EQREL_1:20;
A9: x in the Sorts of U1 -carrier_of (CComp s) by Th5;
assume [x,y] in E . s ; ::_thesis: OSClass (E,x) = OSClass (E,y)
then [x,y] in CompClass (E,(CComp s)) by A8, Def9;
hence OSClass (E,x) = OSClass (E,y) by A9, EQREL_1:35; ::_thesis: verum
end;
theorem :: OSALG_4:13
for S being locally_directed OrderSortedSign
for U1 being non-empty OSAlgebra of S
for E being MSEquivalence-like OrderSortedRelation of U1
for s1, s2 being Element of S
for x being Element of the Sorts of U1 . s1 st s1 <= s2 holds
for y being Element of the Sorts of U1 . s2 st y = x holds
OSClass (E,x) = OSClass (E,y) by Th4;
begin
definition
let S be locally_directed OrderSortedSign;
let o be Element of the carrier' of S;
let A be non-empty OSAlgebra of S;
let R be OSCongruence of A;
let x be Element of Args (o,A);
funcR #_os x -> Element of product ((OSClass R) * (the_arity_of o)) means :Def13: :: OSALG_4:def 13
for n being Nat st n in dom (the_arity_of o) holds
ex y being Element of the Sorts of A . ((the_arity_of o) /. n) st
( y = x . n & it . n = OSClass (R,y) );
existence
ex b1 being Element of product ((OSClass R) * (the_arity_of o)) st
for n being Nat st n in dom (the_arity_of o) holds
ex y being Element of the Sorts of A . ((the_arity_of o) /. n) st
( y = x . n & b1 . n = OSClass (R,y) )
proof
defpred S1[ set , set ] means for n being Nat st n = $1 holds
ex y being Element of the Sorts of A . ((the_arity_of o) /. n) st
( y = x . n & $2 = OSClass (R,y) );
set ar = the_arity_of o;
set da = dom (the_arity_of o);
A1: for k being set st k in dom (the_arity_of o) holds
ex u being set st S1[k,u]
proof
let k be set ; ::_thesis: ( k in dom (the_arity_of o) implies ex u being set st S1[k,u] )
assume A2: k in dom (the_arity_of o) ; ::_thesis: ex u being set st S1[k,u]
then reconsider n = k as Nat ;
reconsider y = x . n as Element of the Sorts of A . ((the_arity_of o) /. n) by A2, MSUALG_6:2;
take OSClass (R,y) ; ::_thesis: S1[k, OSClass (R,y)]
thus S1[k, OSClass (R,y)] ; ::_thesis: verum
end;
consider f being Function such that
A3: ( dom f = dom (the_arity_of o) & ( for x being set st x in dom (the_arity_of o) holds
S1[x,f . x] ) ) from CLASSES1:sch_1(A1);
A4: dom ((OSClass R) * (the_arity_of o)) = dom (the_arity_of o) by PARTFUN1:def_2;
for y being set st y in dom ((OSClass R) * (the_arity_of o)) holds
f . y in ((OSClass R) * (the_arity_of o)) . y
proof
let y be set ; ::_thesis: ( y in dom ((OSClass R) * (the_arity_of o)) implies f . y in ((OSClass R) * (the_arity_of o)) . y )
assume A5: y in dom ((OSClass R) * (the_arity_of o)) ; ::_thesis: f . y in ((OSClass R) * (the_arity_of o)) . y
then reconsider n = y as Nat ;
(the_arity_of o) . y in rng (the_arity_of o) by A4, A5, FUNCT_1:def_3;
then reconsider s = (the_arity_of o) . y as Element of S ;
( ex z being Element of the Sorts of A . ((the_arity_of o) /. n) st
( z = x . n & f . n = OSClass (R,z) ) & (the_arity_of o) /. n = (the_arity_of o) . n ) by A3, A4, A5, PARTFUN1:def_6;
then A6: f . y in OSClass (R,s) ;
((OSClass R) * (the_arity_of o)) . y = (OSClass R) . ((the_arity_of o) . y) by A5, FUNCT_1:12;
hence f . y in ((OSClass R) * (the_arity_of o)) . y by A6, Def11; ::_thesis: verum
end;
then reconsider f = f as Element of product ((OSClass R) * (the_arity_of o)) by A3, A4, CARD_3:9;
take f ; ::_thesis: for n being Nat st n in dom (the_arity_of o) holds
ex y being Element of the Sorts of A . ((the_arity_of o) /. n) st
( y = x . n & f . n = OSClass (R,y) )
let n be Nat; ::_thesis: ( n in dom (the_arity_of o) implies ex y being Element of the Sorts of A . ((the_arity_of o) /. n) st
( y = x . n & f . n = OSClass (R,y) ) )
assume n in dom (the_arity_of o) ; ::_thesis: ex y being Element of the Sorts of A . ((the_arity_of o) /. n) st
( y = x . n & f . n = OSClass (R,y) )
hence ex y being Element of the Sorts of A . ((the_arity_of o) /. n) st
( y = x . n & f . n = OSClass (R,y) ) by A3; ::_thesis: verum
end;
uniqueness
for b1, b2 being Element of product ((OSClass R) * (the_arity_of o)) st ( for n being Nat st n in dom (the_arity_of o) holds
ex y being Element of the Sorts of A . ((the_arity_of o) /. n) st
( y = x . n & b1 . n = OSClass (R,y) ) ) & ( for n being Nat st n in dom (the_arity_of o) holds
ex y being Element of the Sorts of A . ((the_arity_of o) /. n) st
( y = x . n & b2 . n = OSClass (R,y) ) ) holds
b1 = b2
proof
let F, G be Element of product ((OSClass R) * (the_arity_of o)); ::_thesis: ( ( for n being Nat st n in dom (the_arity_of o) holds
ex y being Element of the Sorts of A . ((the_arity_of o) /. n) st
( y = x . n & F . n = OSClass (R,y) ) ) & ( for n being Nat st n in dom (the_arity_of o) holds
ex y being Element of the Sorts of A . ((the_arity_of o) /. n) st
( y = x . n & G . n = OSClass (R,y) ) ) implies F = G )
assume A7: ( ( for n being Nat st n in dom (the_arity_of o) holds
ex y being Element of the Sorts of A . ((the_arity_of o) /. n) st
( y = x . n & F . n = OSClass (R,y) ) ) & ( for n being Nat st n in dom (the_arity_of o) holds
ex y being Element of the Sorts of A . ((the_arity_of o) /. n) st
( y = x . n & G . n = OSClass (R,y) ) ) ) ; ::_thesis: F = G
A8: for y being set st y in dom (the_arity_of o) holds
F . y = G . y
proof
let y be set ; ::_thesis: ( y in dom (the_arity_of o) implies F . y = G . y )
assume A9: y in dom (the_arity_of o) ; ::_thesis: F . y = G . y
then reconsider n = y as Nat ;
( ex z being Element of the Sorts of A . ((the_arity_of o) /. n) st
( z = x . n & F . n = OSClass (R,z) ) & ex z1 being Element of the Sorts of A . ((the_arity_of o) /. n) st
( z1 = x . n & G . n = OSClass (R,z1) ) ) by A7, A9;
hence F . y = G . y ; ::_thesis: verum
end;
A10: dom G = dom (the_arity_of o) by PARTFUN1:def_2;
dom F = dom (the_arity_of o) by PARTFUN1:def_2;
hence F = G by A10, A8, FUNCT_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def13 defines #_os OSALG_4:def_13_:_
for S being locally_directed OrderSortedSign
for o being Element of the carrier' of S
for A being non-empty OSAlgebra of S
for R being OSCongruence of A
for x being Element of Args (o,A)
for b6 being Element of product ((OSClass R) * (the_arity_of o)) holds
( b6 = R #_os x iff for n being Nat st n in dom (the_arity_of o) holds
ex y being Element of the Sorts of A . ((the_arity_of o) /. n) st
( y = x . n & b6 . n = OSClass (R,y) ) );
definition
let S be locally_directed OrderSortedSign;
let o be Element of the carrier' of S;
let A be non-empty OSAlgebra of S;
let R be OSCongruence of A;
func OSQuotRes (R,o) -> Function of (( the Sorts of A * the ResultSort of S) . o),(((OSClass R) * the ResultSort of S) . o) means :Def14: :: OSALG_4:def 14
for x being Element of the Sorts of A . (the_result_sort_of o) holds it . x = OSClass (R,x);
existence
ex b1 being Function of (( the Sorts of A * the ResultSort of S) . o),(((OSClass R) * the ResultSort of S) . o) st
for x being Element of the Sorts of A . (the_result_sort_of o) holds b1 . x = OSClass (R,x)
proof
set rs = the_result_sort_of o;
set D = the Sorts of A . (the_result_sort_of o);
deffunc H1( Element of the Sorts of A . (the_result_sort_of o)) -> Element of OSClass (R,(the_result_sort_of o)) = OSClass (R,$1);
consider f being Function such that
A1: ( dom f = the Sorts of A . (the_result_sort_of o) & ( for d being Element of the Sorts of A . (the_result_sort_of o) holds f . d = H1(d) ) ) from FUNCT_1:sch_4();
A2: for x being set st x in the Sorts of A . (the_result_sort_of o) holds
f . x in (OSClass R) . (the_result_sort_of o)
proof
let x be set ; ::_thesis: ( x in the Sorts of A . (the_result_sort_of o) implies f . x in (OSClass R) . (the_result_sort_of o) )
assume x in the Sorts of A . (the_result_sort_of o) ; ::_thesis: f . x in (OSClass R) . (the_result_sort_of o)
then reconsider x1 = x as Element of the Sorts of A . (the_result_sort_of o) ;
f . x1 = OSClass (R,x1) by A1;
then f . x1 in OSClass (R,(the_result_sort_of o)) ;
hence f . x in (OSClass R) . (the_result_sort_of o) by Def11; ::_thesis: verum
end;
o in the carrier' of S ;
then o in dom ( the Sorts of A * the ResultSort of S) by PARTFUN1:def_2;
then A3: ( the Sorts of A * the ResultSort of S) . o = the Sorts of A . ( the ResultSort of S . o) by FUNCT_1:12
.= the Sorts of A . (the_result_sort_of o) by MSUALG_1:def_2 ;
A4: dom the ResultSort of S = the carrier' of S by FUNCT_2:def_1;
then dom ((OSClass R) * the ResultSort of S) = dom the ResultSort of S by PARTFUN1:def_2;
then ((OSClass R) * the ResultSort of S) . o = (OSClass R) . ( the ResultSort of S . o) by A4, FUNCT_1:12
.= (OSClass R) . (the_result_sort_of o) by MSUALG_1:def_2 ;
then reconsider f = f as Function of (( the Sorts of A * the ResultSort of S) . o),(((OSClass R) * the ResultSort of S) . o) by A1, A3, A2, FUNCT_2:3;
take f ; ::_thesis: for x being Element of the Sorts of A . (the_result_sort_of o) holds f . x = OSClass (R,x)
thus for x being Element of the Sorts of A . (the_result_sort_of o) holds f . x = OSClass (R,x) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of (( the Sorts of A * the ResultSort of S) . o),(((OSClass R) * the ResultSort of S) . o) st ( for x being Element of the Sorts of A . (the_result_sort_of o) holds b1 . x = OSClass (R,x) ) & ( for x being Element of the Sorts of A . (the_result_sort_of o) holds b2 . x = OSClass (R,x) ) holds
b1 = b2
proof
set SA = the Sorts of A;
set RS = the ResultSort of S;
set rs = the_result_sort_of o;
let f, g be Function of (( the Sorts of A * the ResultSort of S) . o),(((OSClass R) * the ResultSort of S) . o); ::_thesis: ( ( for x being Element of the Sorts of A . (the_result_sort_of o) holds f . x = OSClass (R,x) ) & ( for x being Element of the Sorts of A . (the_result_sort_of o) holds g . x = OSClass (R,x) ) implies f = g )
assume that
A5: for x being Element of the Sorts of A . (the_result_sort_of o) holds f . x = OSClass (R,x) and
A6: for x being Element of the Sorts of A . (the_result_sort_of o) holds g . x = OSClass (R,x) ; ::_thesis: f = g
A7: now__::_thesis:_for_x_being_set_st_x_in_the_Sorts_of_A_._(the_result_sort_of_o)_holds_
f_._x_=_g_._x
let x be set ; ::_thesis: ( x in the Sorts of A . (the_result_sort_of o) implies f . x = g . x )
assume x in the Sorts of A . (the_result_sort_of o) ; ::_thesis: f . x = g . x
then reconsider x1 = x as Element of the Sorts of A . (the_result_sort_of o) ;
f . x1 = OSClass (R,x1) by A5;
hence f . x = g . x by A6; ::_thesis: verum
end;
o in the carrier' of S ;
then o in dom ( the Sorts of A * the ResultSort of S) by PARTFUN1:def_2;
then ( the Sorts of A * the ResultSort of S) . o = the Sorts of A . ( the ResultSort of S . o) by FUNCT_1:12
.= the Sorts of A . (the_result_sort_of o) by MSUALG_1:def_2 ;
then ( dom f = the Sorts of A . (the_result_sort_of o) & dom g = the Sorts of A . (the_result_sort_of o) ) by FUNCT_2:def_1;
hence f = g by A7, FUNCT_1:2; ::_thesis: verum
end;
func OSQuotArgs (R,o) -> Function of ((( the Sorts of A #) * the Arity of S) . o),((((OSClass R) #) * the Arity of S) . o) means :: OSALG_4:def 15
for x being Element of Args (o,A) holds it . x = R #_os x;
existence
ex b1 being Function of ((( the Sorts of A #) * the Arity of S) . o),((((OSClass R) #) * the Arity of S) . o) st
for x being Element of Args (o,A) holds b1 . x = R #_os x
proof
set ao = the_arity_of o;
set D = Args (o,A);
deffunc H1( Element of Args (o,A)) -> Element of product ((OSClass R) * (the_arity_of o)) = R #_os $1;
consider f being Function such that
A8: ( dom f = Args (o,A) & ( for d being Element of Args (o,A) holds f . d = H1(d) ) ) from FUNCT_1:sch_4();
A9: o in the carrier' of S ;
then o in dom (( the Sorts of A #) * the Arity of S) by PARTFUN1:def_2;
then A10: (( the Sorts of A #) * the Arity of S) . o = ( the Sorts of A #) . ( the Arity of S . o) by FUNCT_1:12
.= ( the Sorts of A #) . (the_arity_of o) by MSUALG_1:def_1 ;
A11: for x being set st x in ( the Sorts of A #) . (the_arity_of o) holds
f . x in ((OSClass R) #) . (the_arity_of o)
proof
let x be set ; ::_thesis: ( x in ( the Sorts of A #) . (the_arity_of o) implies f . x in ((OSClass R) #) . (the_arity_of o) )
assume x in ( the Sorts of A #) . (the_arity_of o) ; ::_thesis: f . x in ((OSClass R) #) . (the_arity_of o)
then reconsider x1 = x as Element of Args (o,A) by A10, MSUALG_1:def_4;
( f . x1 = R #_os x1 & ((OSClass R) #) . (the_arity_of o) = product ((OSClass R) * (the_arity_of o)) ) by A8, FINSEQ_2:def_5;
hence f . x in ((OSClass R) #) . (the_arity_of o) ; ::_thesis: verum
end;
o in dom (((OSClass R) #) * the Arity of S) by A9, PARTFUN1:def_2;
then (((OSClass R) #) * the Arity of S) . o = ((OSClass R) #) . ( the Arity of S . o) by FUNCT_1:12
.= ((OSClass R) #) . (the_arity_of o) by MSUALG_1:def_1 ;
then reconsider f = f as Function of ((( the Sorts of A #) * the Arity of S) . o),((((OSClass R) #) * the Arity of S) . o) by A8, A10, A11, FUNCT_2:3, MSUALG_1:def_4;
take f ; ::_thesis: for x being Element of Args (o,A) holds f . x = R #_os x
thus for x being Element of Args (o,A) holds f . x = R #_os x by A8; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of ((( the Sorts of A #) * the Arity of S) . o),((((OSClass R) #) * the Arity of S) . o) st ( for x being Element of Args (o,A) holds b1 . x = R #_os x ) & ( for x being Element of Args (o,A) holds b2 . x = R #_os x ) holds
b1 = b2
proof
set ao = the_arity_of o;
let f, g be Function of ((( the Sorts of A #) * the Arity of S) . o),((((OSClass R) #) * the Arity of S) . o); ::_thesis: ( ( for x being Element of Args (o,A) holds f . x = R #_os x ) & ( for x being Element of Args (o,A) holds g . x = R #_os x ) implies f = g )
assume that
A12: for x being Element of Args (o,A) holds f . x = R #_os x and
A13: for x being Element of Args (o,A) holds g . x = R #_os x ; ::_thesis: f = g
o in the carrier' of S ;
then o in dom (( the Sorts of A #) * the Arity of S) by PARTFUN1:def_2;
then A14: (( the Sorts of A #) * the Arity of S) . o = ( the Sorts of A #) . ( the Arity of S . o) by FUNCT_1:12
.= ( the Sorts of A #) . (the_arity_of o) by MSUALG_1:def_1 ;
A15: now__::_thesis:_for_x_being_set_st_x_in_(_the_Sorts_of_A_#)_._(the_arity_of_o)_holds_
f_._x_=_g_._x
let x be set ; ::_thesis: ( x in ( the Sorts of A #) . (the_arity_of o) implies f . x = g . x )
assume x in ( the Sorts of A #) . (the_arity_of o) ; ::_thesis: f . x = g . x
then reconsider x1 = x as Element of Args (o,A) by A14, MSUALG_1:def_4;
f . x1 = R #_os x1 by A12;
hence f . x = g . x by A13; ::_thesis: verum
end;
( dom f = ( the Sorts of A #) . (the_arity_of o) & dom g = ( the Sorts of A #) . (the_arity_of o) ) by A14, FUNCT_2:def_1;
hence f = g by A15, FUNCT_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def14 defines OSQuotRes OSALG_4:def_14_:_
for S being locally_directed OrderSortedSign
for o being Element of the carrier' of S
for A being non-empty OSAlgebra of S
for R being OSCongruence of A
for b5 being Function of (( the Sorts of A * the ResultSort of S) . o),(((OSClass R) * the ResultSort of S) . o) holds
( b5 = OSQuotRes (R,o) iff for x being Element of the Sorts of A . (the_result_sort_of o) holds b5 . x = OSClass (R,x) );
:: deftheorem defines OSQuotArgs OSALG_4:def_15_:_
for S being locally_directed OrderSortedSign
for o being Element of the carrier' of S
for A being non-empty OSAlgebra of S
for R being OSCongruence of A
for b5 being Function of ((( the Sorts of A #) * the Arity of S) . o),((((OSClass R) #) * the Arity of S) . o) holds
( b5 = OSQuotArgs (R,o) iff for x being Element of Args (o,A) holds b5 . x = R #_os x );
definition
let S be locally_directed OrderSortedSign;
let A be non-empty OSAlgebra of S;
let R be OSCongruence of A;
func OSQuotRes R -> ManySortedFunction of the Sorts of A * the ResultSort of S,(OSClass R) * the ResultSort of S means :: OSALG_4:def 16
for o being OperSymbol of S holds it . o = OSQuotRes (R,o);
existence
ex b1 being ManySortedFunction of the Sorts of A * the ResultSort of S,(OSClass R) * the ResultSort of S st
for o being OperSymbol of S holds b1 . o = OSQuotRes (R,o)
proof
defpred S1[ set , set ] means for o being OperSymbol of S st o = $1 holds
$2 = OSQuotRes (R,o);
set O = the carrier' of S;
A1: for x being set st x in the carrier' of S holds
ex y being set st S1[x,y]
proof
let x be set ; ::_thesis: ( x in the carrier' of S implies ex y being set st S1[x,y] )
assume x in the carrier' of S ; ::_thesis: ex y being set st S1[x,y]
then reconsider x1 = x as OperSymbol of S ;
take OSQuotRes (R,x1) ; ::_thesis: S1[x, OSQuotRes (R,x1)]
thus S1[x, OSQuotRes (R,x1)] ; ::_thesis: verum
end;
consider f being Function such that
A2: ( dom f = the carrier' of S & ( for x being set st x in the carrier' of S holds
S1[x,f . x] ) ) from CLASSES1:sch_1(A1);
reconsider f = f as ManySortedSet of the carrier' of S by A2, PARTFUN1:def_2, RELAT_1:def_18;
for x being set st x in dom f holds
f . x is Function
proof
let x be set ; ::_thesis: ( x in dom f implies f . x is Function )
assume x in dom f ; ::_thesis: f . x is Function
then reconsider x1 = x as OperSymbol of S ;
f . x1 = OSQuotRes (R,x1) by A2;
hence f . x is Function ; ::_thesis: verum
end;
then reconsider f = f as ManySortedFunction of the carrier' of S by FUNCOP_1:def_6;
for i being set st i in the carrier' of S holds
f . i is Function of (( the Sorts of A * the ResultSort of S) . i),(((OSClass R) * the ResultSort of S) . i)
proof
let i be set ; ::_thesis: ( i in the carrier' of S implies f . i is Function of (( the Sorts of A * the ResultSort of S) . i),(((OSClass R) * the ResultSort of S) . i) )
assume i in the carrier' of S ; ::_thesis: f . i is Function of (( the Sorts of A * the ResultSort of S) . i),(((OSClass R) * the ResultSort of S) . i)
then reconsider i1 = i as OperSymbol of S ;
f . i1 = OSQuotRes (R,i1) by A2;
hence f . i is Function of (( the Sorts of A * the ResultSort of S) . i),(((OSClass R) * the ResultSort of S) . i) ; ::_thesis: verum
end;
then reconsider f = f as ManySortedFunction of the Sorts of A * the ResultSort of S,(OSClass R) * the ResultSort of S by PBOOLE:def_15;
take f ; ::_thesis: for o being OperSymbol of S holds f . o = OSQuotRes (R,o)
thus for o being OperSymbol of S holds f . o = OSQuotRes (R,o) by A2; ::_thesis: verum
end;
uniqueness
for b1, b2 being ManySortedFunction of the Sorts of A * the ResultSort of S,(OSClass R) * the ResultSort of S st ( for o being OperSymbol of S holds b1 . o = OSQuotRes (R,o) ) & ( for o being OperSymbol of S holds b2 . o = OSQuotRes (R,o) ) holds
b1 = b2
proof
let f, g be ManySortedFunction of the Sorts of A * the ResultSort of S,(OSClass R) * the ResultSort of S; ::_thesis: ( ( for o being OperSymbol of S holds f . o = OSQuotRes (R,o) ) & ( for o being OperSymbol of S holds g . o = OSQuotRes (R,o) ) implies f = g )
assume that
A3: for o being OperSymbol of S holds f . o = OSQuotRes (R,o) and
A4: for o being OperSymbol of S holds g . o = OSQuotRes (R,o) ; ::_thesis: f = g
now__::_thesis:_for_i_being_set_st_i_in_the_carrier'_of_S_holds_
f_._i_=_g_._i
let i be set ; ::_thesis: ( i in the carrier' of S implies f . i = g . i )
assume i in the carrier' of S ; ::_thesis: f . i = g . i
then reconsider i1 = i as OperSymbol of S ;
f . i1 = OSQuotRes (R,i1) by A3;
hence f . i = g . i by A4; ::_thesis: verum
end;
hence f = g by PBOOLE:3; ::_thesis: verum
end;
func OSQuotArgs R -> ManySortedFunction of ( the Sorts of A #) * the Arity of S,((OSClass R) #) * the Arity of S means :: OSALG_4:def 17
for o being OperSymbol of S holds it . o = OSQuotArgs (R,o);
existence
ex b1 being ManySortedFunction of ( the Sorts of A #) * the Arity of S,((OSClass R) #) * the Arity of S st
for o being OperSymbol of S holds b1 . o = OSQuotArgs (R,o)
proof
defpred S1[ set , set ] means for o being OperSymbol of S st o = $1 holds
$2 = OSQuotArgs (R,o);
set O = the carrier' of S;
A5: for x being set st x in the carrier' of S holds
ex y being set st S1[x,y]
proof
let x be set ; ::_thesis: ( x in the carrier' of S implies ex y being set st S1[x,y] )
assume x in the carrier' of S ; ::_thesis: ex y being set st S1[x,y]
then reconsider x1 = x as OperSymbol of S ;
take OSQuotArgs (R,x1) ; ::_thesis: S1[x, OSQuotArgs (R,x1)]
thus S1[x, OSQuotArgs (R,x1)] ; ::_thesis: verum
end;
consider f being Function such that
A6: ( dom f = the carrier' of S & ( for x being set st x in the carrier' of S holds
S1[x,f . x] ) ) from CLASSES1:sch_1(A5);
reconsider f = f as ManySortedSet of the carrier' of S by A6, PARTFUN1:def_2, RELAT_1:def_18;
for x being set st x in dom f holds
f . x is Function
proof
let x be set ; ::_thesis: ( x in dom f implies f . x is Function )
assume x in dom f ; ::_thesis: f . x is Function
then reconsider x1 = x as OperSymbol of S ;
f . x1 = OSQuotArgs (R,x1) by A6;
hence f . x is Function ; ::_thesis: verum
end;
then reconsider f = f as ManySortedFunction of the carrier' of S by FUNCOP_1:def_6;
for i being set st i in the carrier' of S holds
f . i is Function of ((( the Sorts of A #) * the Arity of S) . i),((((OSClass R) #) * the Arity of S) . i)
proof
let i be set ; ::_thesis: ( i in the carrier' of S implies f . i is Function of ((( the Sorts of A #) * the Arity of S) . i),((((OSClass R) #) * the Arity of S) . i) )
assume i in the carrier' of S ; ::_thesis: f . i is Function of ((( the Sorts of A #) * the Arity of S) . i),((((OSClass R) #) * the Arity of S) . i)
then reconsider i1 = i as OperSymbol of S ;
f . i1 = OSQuotArgs (R,i1) by A6;
hence f . i is Function of ((( the Sorts of A #) * the Arity of S) . i),((((OSClass R) #) * the Arity of S) . i) ; ::_thesis: verum
end;
then reconsider f = f as ManySortedFunction of ( the Sorts of A #) * the Arity of S,((OSClass R) #) * the Arity of S by PBOOLE:def_15;
take f ; ::_thesis: for o being OperSymbol of S holds f . o = OSQuotArgs (R,o)
thus for o being OperSymbol of S holds f . o = OSQuotArgs (R,o) by A6; ::_thesis: verum
end;
uniqueness
for b1, b2 being ManySortedFunction of ( the Sorts of A #) * the Arity of S,((OSClass R) #) * the Arity of S st ( for o being OperSymbol of S holds b1 . o = OSQuotArgs (R,o) ) & ( for o being OperSymbol of S holds b2 . o = OSQuotArgs (R,o) ) holds
b1 = b2
proof
let f, g be ManySortedFunction of ( the Sorts of A #) * the Arity of S,((OSClass R) #) * the Arity of S; ::_thesis: ( ( for o being OperSymbol of S holds f . o = OSQuotArgs (R,o) ) & ( for o being OperSymbol of S holds g . o = OSQuotArgs (R,o) ) implies f = g )
assume that
A7: for o being OperSymbol of S holds f . o = OSQuotArgs (R,o) and
A8: for o being OperSymbol of S holds g . o = OSQuotArgs (R,o) ; ::_thesis: f = g
now__::_thesis:_for_i_being_set_st_i_in_the_carrier'_of_S_holds_
f_._i_=_g_._i
let i be set ; ::_thesis: ( i in the carrier' of S implies f . i = g . i )
assume i in the carrier' of S ; ::_thesis: f . i = g . i
then reconsider i1 = i as OperSymbol of S ;
f . i1 = OSQuotArgs (R,i1) by A7;
hence f . i = g . i by A8; ::_thesis: verum
end;
hence f = g by PBOOLE:3; ::_thesis: verum
end;
end;
:: deftheorem defines OSQuotRes OSALG_4:def_16_:_
for S being locally_directed OrderSortedSign
for A being non-empty OSAlgebra of S
for R being OSCongruence of A
for b4 being ManySortedFunction of the Sorts of A * the ResultSort of S,(OSClass R) * the ResultSort of S holds
( b4 = OSQuotRes R iff for o being OperSymbol of S holds b4 . o = OSQuotRes (R,o) );
:: deftheorem defines OSQuotArgs OSALG_4:def_17_:_
for S being locally_directed OrderSortedSign
for A being non-empty OSAlgebra of S
for R being OSCongruence of A
for b4 being ManySortedFunction of ( the Sorts of A #) * the Arity of S,((OSClass R) #) * the Arity of S holds
( b4 = OSQuotArgs R iff for o being OperSymbol of S holds b4 . o = OSQuotArgs (R,o) );
theorem Th14: :: OSALG_4:14
for S being locally_directed OrderSortedSign
for o being Element of the carrier' of S
for A being non-empty OSAlgebra of S
for R being OSCongruence of A
for x being set st x in (((OSClass R) #) * the Arity of S) . o holds
ex a being Element of Args (o,A) st x = R #_os a
proof
let S be locally_directed OrderSortedSign; ::_thesis: for o being Element of the carrier' of S
for A being non-empty OSAlgebra of S
for R being OSCongruence of A
for x being set st x in (((OSClass R) #) * the Arity of S) . o holds
ex a being Element of Args (o,A) st x = R #_os a
let o be Element of the carrier' of S; ::_thesis: for A being non-empty OSAlgebra of S
for R being OSCongruence of A
for x being set st x in (((OSClass R) #) * the Arity of S) . o holds
ex a being Element of Args (o,A) st x = R #_os a
let A be non-empty OSAlgebra of S; ::_thesis: for R being OSCongruence of A
for x being set st x in (((OSClass R) #) * the Arity of S) . o holds
ex a being Element of Args (o,A) st x = R #_os a
let R be OSCongruence of A; ::_thesis: for x being set st x in (((OSClass R) #) * the Arity of S) . o holds
ex a being Element of Args (o,A) st x = R #_os a
let x be set ; ::_thesis: ( x in (((OSClass R) #) * the Arity of S) . o implies ex a being Element of Args (o,A) st x = R #_os a )
assume A1: x in (((OSClass R) #) * the Arity of S) . o ; ::_thesis: ex a being Element of Args (o,A) st x = R #_os a
set ar = the_arity_of o;
A2: the_arity_of o = the Arity of S . o by MSUALG_1:def_1;
then (((OSClass R) #) * the Arity of S) . o = product ((OSClass R) * (the_arity_of o)) by MSAFREE:1;
then consider f being Function such that
A3: f = x and
A4: dom f = dom ((OSClass R) * (the_arity_of o)) and
A5: for y being set st y in dom ((OSClass R) * (the_arity_of o)) holds
f . y in ((OSClass R) * (the_arity_of o)) . y by A1, CARD_3:def_5;
defpred S1[ set , set ] means ( $2 in the Sorts of A . ((the_arity_of o) /. $1) & $2 in f . $1 );
A6: dom ((OSClass R) * (the_arity_of o)) = dom (the_arity_of o) by PARTFUN1:def_2;
A7: for n being Nat st n in dom f holds
f . n in OSClass (R,((the_arity_of o) /. n))
proof
let n be Nat; ::_thesis: ( n in dom f implies f . n in OSClass (R,((the_arity_of o) /. n)) )
reconsider s = (the_arity_of o) /. n as Element of S ;
assume A8: n in dom f ; ::_thesis: f . n in OSClass (R,((the_arity_of o) /. n))
then (the_arity_of o) . n = (the_arity_of o) /. n by A4, A6, PARTFUN1:def_6;
then ((OSClass R) * (the_arity_of o)) . n = (OSClass R) . s by A4, A8, FUNCT_1:12
.= OSClass (R,s) by Def11 ;
hence f . n in OSClass (R,((the_arity_of o) /. n)) by A4, A5, A8; ::_thesis: verum
end;
A9: for a being set st a in dom f holds
ex b being set st S1[a,b]
proof
let a be set ; ::_thesis: ( a in dom f implies ex b being set st S1[a,b] )
reconsider s = (the_arity_of o) /. a as Element of S ;
assume A10: a in dom f ; ::_thesis: ex b being set st S1[a,b]
then reconsider n = a as Nat by A4;
f . n in OSClass (R,s) by A7, A10;
then consider x being set such that
A11: ( x in the Sorts of A . s & f . n = Class ((CompClass (R,(CComp s))),x) ) by Def10;
take x ; ::_thesis: S1[a,x]
thus S1[a,x] by A11, Th5, EQREL_1:20; ::_thesis: verum
end;
consider g being Function such that
A12: ( dom g = dom f & ( for a being set st a in dom f holds
S1[a,g . a] ) ) from CLASSES1:sch_1(A9);
dom the Sorts of A = the carrier of S by PARTFUN1:def_2;
then rng (the_arity_of o) c= dom the Sorts of A ;
then A13: dom g = dom ( the Sorts of A * (the_arity_of o)) by A4, A6, A12, RELAT_1:27;
A14: for y being set st y in dom ( the Sorts of A * (the_arity_of o)) holds
g . y in ( the Sorts of A * (the_arity_of o)) . y
proof
let y be set ; ::_thesis: ( y in dom ( the Sorts of A * (the_arity_of o)) implies g . y in ( the Sorts of A * (the_arity_of o)) . y )
assume A15: y in dom ( the Sorts of A * (the_arity_of o)) ; ::_thesis: g . y in ( the Sorts of A * (the_arity_of o)) . y
then reconsider n = y as Nat ;
reconsider s = (the_arity_of o) /. n as Element of S ;
( (the_arity_of o) . n = (the_arity_of o) /. n & g . n in the Sorts of A . s ) by A4, A6, A12, A13, A15, PARTFUN1:def_6;
hence g . y in ( the Sorts of A * (the_arity_of o)) . y by A15, FUNCT_1:12; ::_thesis: verum
end;
Args (o,A) = (( the Sorts of A #) * the Arity of S) . o by MSUALG_1:def_4
.= product ( the Sorts of A * (the_arity_of o)) by A2, MSAFREE:1 ;
then reconsider g = g as Element of Args (o,A) by A13, A14, CARD_3:9;
A16: for x being set st x in dom (the_arity_of o) holds
f . x = (R #_os g) . x
proof
let x be set ; ::_thesis: ( x in dom (the_arity_of o) implies f . x = (R #_os g) . x )
assume A17: x in dom (the_arity_of o) ; ::_thesis: f . x = (R #_os g) . x
then reconsider n = x as Nat ;
A18: ( ex z being Element of the Sorts of A . ((the_arity_of o) /. n) st
( z = g . n & (R #_os g) . n = OSClass (R,z) ) & g . n in f . n ) by A4, A6, A12, A17, Def13;
reconsider s = (the_arity_of o) /. n as Element of S ;
f . n in OSClass (R,s) by A4, A6, A7, A17;
then consider u being set such that
A19: u in the Sorts of A . s and
A20: f . n = Class ((CompClass (R,(CComp s))),u) by Def10;
u in the Sorts of A -carrier_of (CComp s) by A19, Th5;
hence f . x = (R #_os g) . x by A18, A20, EQREL_1:23; ::_thesis: verum
end;
take g ; ::_thesis: x = R #_os g
dom (R #_os g) = dom ((OSClass R) * (the_arity_of o)) by CARD_3:9;
hence x = R #_os g by A3, A4, A6, A16, FUNCT_1:2; ::_thesis: verum
end;
definition
let S be locally_directed OrderSortedSign;
let o be Element of the carrier' of S;
let A be non-empty OSAlgebra of S;
let R be OSCongruence of A;
func OSQuotCharact (R,o) -> Function of ((((OSClass R) #) * the Arity of S) . o),(((OSClass R) * the ResultSort of S) . o) means :Def18: :: OSALG_4:def 18
for a being Element of Args (o,A) st R #_os a in (((OSClass R) #) * the Arity of S) . o holds
it . (R #_os a) = ((OSQuotRes (R,o)) * (Den (o,A))) . a;
existence
ex b1 being Function of ((((OSClass R) #) * the Arity of S) . o),(((OSClass R) * the ResultSort of S) . o) st
for a being Element of Args (o,A) st R #_os a in (((OSClass R) #) * the Arity of S) . o holds
b1 . (R #_os a) = ((OSQuotRes (R,o)) * (Den (o,A))) . a
proof
defpred S1[ set , set ] means for a being Element of Args (o,A) st $1 = R #_os a holds
$2 = ((OSQuotRes (R,o)) * (Den (o,A))) . a;
set Ca = (((OSClass R) #) * the Arity of S) . o;
set Cr = ((OSClass R) * the ResultSort of S) . o;
A1: for x being set st x in (((OSClass R) #) * the Arity of S) . o holds
ex y being set st
( y in ((OSClass R) * the ResultSort of S) . o & S1[x,y] )
proof
set ro = the_result_sort_of o;
set ar = the_arity_of o;
let x be set ; ::_thesis: ( x in (((OSClass R) #) * the Arity of S) . o implies ex y being set st
( y in ((OSClass R) * the ResultSort of S) . o & S1[x,y] ) )
assume x in (((OSClass R) #) * the Arity of S) . o ; ::_thesis: ex y being set st
( y in ((OSClass R) * the ResultSort of S) . o & S1[x,y] )
then consider a being Element of Args (o,A) such that
A2: x = R #_os a by Th14;
take y = ((OSQuotRes (R,o)) * (Den (o,A))) . a; ::_thesis: ( y in ((OSClass R) * the ResultSort of S) . o & S1[x,y] )
A3: o in the carrier' of S ;
then o in dom ((OSClass R) * the ResultSort of S) by PARTFUN1:def_2;
then A4: ((OSClass R) * the ResultSort of S) . o = (OSClass R) . ( the ResultSort of S . o) by FUNCT_1:12
.= (OSClass R) . (the_result_sort_of o) by MSUALG_1:def_2 ;
o in dom ( the Sorts of A * the ResultSort of S) by A3, PARTFUN1:def_2;
then A5: ( the Sorts of A * the ResultSort of S) . o = the Sorts of A . ( the ResultSort of S . o) by FUNCT_1:12
.= the Sorts of A . (the_result_sort_of o) by MSUALG_1:def_2 ;
then A6: ( dom (OSQuotRes (R,o)) = the Sorts of A . (the_result_sort_of o) & Result (o,A) = the Sorts of A . (the_result_sort_of o) ) by FUNCT_2:def_1, MSUALG_1:def_5;
rng (Den (o,A)) c= Result (o,A) ;
then A7: ( dom (Den (o,A)) = Args (o,A) & dom ((OSQuotRes (R,o)) * (Den (o,A))) = dom (Den (o,A)) ) by A6, FUNCT_2:def_1, RELAT_1:27;
(OSQuotRes (R,o)) . ((Den (o,A)) . a) in rng (OSQuotRes (R,o)) by A6, FUNCT_1:def_3;
then (OSQuotRes (R,o)) . ((Den (o,A)) . a) in (OSClass R) . (the_result_sort_of o) by A4;
hence y in ((OSClass R) * the ResultSort of S) . o by A4, A7, FUNCT_1:12; ::_thesis: S1[x,y]
let b be Element of Args (o,A); ::_thesis: ( x = R #_os b implies y = ((OSQuotRes (R,o)) * (Den (o,A))) . b )
reconsider da = (Den (o,A)) . a, db = (Den (o,A)) . b as Element of the Sorts of A . (the_result_sort_of o) by A5, MSUALG_1:def_5;
A8: ((OSQuotRes (R,o)) * (Den (o,A))) . b = (OSQuotRes (R,o)) . db by A7, FUNCT_1:12
.= OSClass (R,db) by Def14
.= Class ((CompClass (R,(CComp (the_result_sort_of o)))),db) ;
assume A9: x = R #_os b ; ::_thesis: y = ((OSQuotRes (R,o)) * (Den (o,A))) . b
for n being Nat st n in dom a holds
[(a . n),(b . n)] in R . ((the_arity_of o) /. n)
proof
let n be Nat; ::_thesis: ( n in dom a implies [(a . n),(b . n)] in R . ((the_arity_of o) /. n) )
A10: dom a = dom (the_arity_of o) by MSUALG_3:6;
assume n in dom a ; ::_thesis: [(a . n),(b . n)] in R . ((the_arity_of o) /. n)
then ( ex ya being Element of the Sorts of A . ((the_arity_of o) /. n) st
( ya = a . n & (R #_os a) . n = OSClass (R,ya) ) & ex yb being Element of the Sorts of A . ((the_arity_of o) /. n) st
( yb = b . n & (R #_os b) . n = OSClass (R,yb) ) ) by A10, Def13;
hence [(a . n),(b . n)] in R . ((the_arity_of o) /. n) by A2, A9, Th12; ::_thesis: verum
end;
then ( the_result_sort_of o in CComp (the_result_sort_of o) & [da,db] in R . (the_result_sort_of o) ) by EQREL_1:20, MSUALG_4:def_4;
then A11: [da,db] in CompClass (R,(CComp (the_result_sort_of o))) by Def9;
A12: da in the Sorts of A -carrier_of (CComp (the_result_sort_of o)) by Th5;
y = (OSQuotRes (R,o)) . ((Den (o,A)) . a) by A7, FUNCT_1:12
.= OSClass (R,da) by Def14
.= Class ((CompClass (R,(CComp (the_result_sort_of o)))),da) ;
hence y = ((OSQuotRes (R,o)) * (Den (o,A))) . b by A12, A8, A11, EQREL_1:35; ::_thesis: verum
end;
consider f being Function such that
A13: ( dom f = (((OSClass R) #) * the Arity of S) . o & rng f c= ((OSClass R) * the ResultSort of S) . o & ( for x being set st x in (((OSClass R) #) * the Arity of S) . o holds
S1[x,f . x] ) ) from FUNCT_1:sch_5(A1);
reconsider f = f as Function of ((((OSClass R) #) * the Arity of S) . o),(((OSClass R) * the ResultSort of S) . o) by A13, FUNCT_2:2;
take f ; ::_thesis: for a being Element of Args (o,A) st R #_os a in (((OSClass R) #) * the Arity of S) . o holds
f . (R #_os a) = ((OSQuotRes (R,o)) * (Den (o,A))) . a
thus for a being Element of Args (o,A) st R #_os a in (((OSClass R) #) * the Arity of S) . o holds
f . (R #_os a) = ((OSQuotRes (R,o)) * (Den (o,A))) . a by A13; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of ((((OSClass R) #) * the Arity of S) . o),(((OSClass R) * the ResultSort of S) . o) st ( for a being Element of Args (o,A) st R #_os a in (((OSClass R) #) * the Arity of S) . o holds
b1 . (R #_os a) = ((OSQuotRes (R,o)) * (Den (o,A))) . a ) & ( for a being Element of Args (o,A) st R #_os a in (((OSClass R) #) * the Arity of S) . o holds
b2 . (R #_os a) = ((OSQuotRes (R,o)) * (Den (o,A))) . a ) holds
b1 = b2
proof
set ao = the_arity_of o;
let F, G be Function of ((((OSClass R) #) * the Arity of S) . o),(((OSClass R) * the ResultSort of S) . o); ::_thesis: ( ( for a being Element of Args (o,A) st R #_os a in (((OSClass R) #) * the Arity of S) . o holds
F . (R #_os a) = ((OSQuotRes (R,o)) * (Den (o,A))) . a ) & ( for a being Element of Args (o,A) st R #_os a in (((OSClass R) #) * the Arity of S) . o holds
G . (R #_os a) = ((OSQuotRes (R,o)) * (Den (o,A))) . a ) implies F = G )
assume that
A14: for a being Element of Args (o,A) st R #_os a in (((OSClass R) #) * the Arity of S) . o holds
F . (R #_os a) = ((OSQuotRes (R,o)) * (Den (o,A))) . a and
A15: for a being Element of Args (o,A) st R #_os a in (((OSClass R) #) * the Arity of S) . o holds
G . (R #_os a) = ((OSQuotRes (R,o)) * (Den (o,A))) . a ; ::_thesis: F = G
A16: dom the Arity of S = the carrier' of S by FUNCT_2:def_1;
then dom (((OSClass R) #) * the Arity of S) = dom the Arity of S by PARTFUN1:def_2;
then A17: (((OSClass R) #) * the Arity of S) . o = ((OSClass R) #) . ( the Arity of S . o) by A16, FUNCT_1:12
.= ((OSClass R) #) . (the_arity_of o) by MSUALG_1:def_1 ;
A18: now__::_thesis:_for_x_being_set_st_x_in_((OSClass_R)_#)_._(the_arity_of_o)_holds_
F_._x_=_G_._x
let x be set ; ::_thesis: ( x in ((OSClass R) #) . (the_arity_of o) implies F . x = G . x )
assume A19: x in ((OSClass R) #) . (the_arity_of o) ; ::_thesis: F . x = G . x
then consider a being Element of Args (o,A) such that
A20: x = R #_os a by A17, Th14;
F . x = ((OSQuotRes (R,o)) * (Den (o,A))) . a by A14, A17, A19, A20;
hence F . x = G . x by A15, A17, A19, A20; ::_thesis: verum
end;
( dom F = ((OSClass R) #) . (the_arity_of o) & dom G = ((OSClass R) #) . (the_arity_of o) ) by A17, FUNCT_2:def_1;
hence F = G by A18, FUNCT_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def18 defines OSQuotCharact OSALG_4:def_18_:_
for S being locally_directed OrderSortedSign
for o being Element of the carrier' of S
for A being non-empty OSAlgebra of S
for R being OSCongruence of A
for b5 being Function of ((((OSClass R) #) * the Arity of S) . o),(((OSClass R) * the ResultSort of S) . o) holds
( b5 = OSQuotCharact (R,o) iff for a being Element of Args (o,A) st R #_os a in (((OSClass R) #) * the Arity of S) . o holds
b5 . (R #_os a) = ((OSQuotRes (R,o)) * (Den (o,A))) . a );
definition
let S be locally_directed OrderSortedSign;
let A be non-empty OSAlgebra of S;
let R be OSCongruence of A;
func OSQuotCharact R -> ManySortedFunction of ((OSClass R) #) * the Arity of S,(OSClass R) * the ResultSort of S means :Def19: :: OSALG_4:def 19
for o being OperSymbol of S holds it . o = OSQuotCharact (R,o);
existence
ex b1 being ManySortedFunction of ((OSClass R) #) * the Arity of S,(OSClass R) * the ResultSort of S st
for o being OperSymbol of S holds b1 . o = OSQuotCharact (R,o)
proof
defpred S1[ set , set ] means for o being OperSymbol of S st o = $1 holds
$2 = OSQuotCharact (R,o);
set O = the carrier' of S;
A1: for x being set st x in the carrier' of S holds
ex y being set st S1[x,y]
proof
let x be set ; ::_thesis: ( x in the carrier' of S implies ex y being set st S1[x,y] )
assume x in the carrier' of S ; ::_thesis: ex y being set st S1[x,y]
then reconsider x1 = x as OperSymbol of S ;
take OSQuotCharact (R,x1) ; ::_thesis: S1[x, OSQuotCharact (R,x1)]
thus S1[x, OSQuotCharact (R,x1)] ; ::_thesis: verum
end;
consider f being Function such that
A2: ( dom f = the carrier' of S & ( for x being set st x in the carrier' of S holds
S1[x,f . x] ) ) from CLASSES1:sch_1(A1);
reconsider f = f as ManySortedSet of the carrier' of S by A2, PARTFUN1:def_2, RELAT_1:def_18;
for x being set st x in dom f holds
f . x is Function
proof
let x be set ; ::_thesis: ( x in dom f implies f . x is Function )
assume x in dom f ; ::_thesis: f . x is Function
then reconsider x1 = x as OperSymbol of S ;
f . x1 = OSQuotCharact (R,x1) by A2;
hence f . x is Function ; ::_thesis: verum
end;
then reconsider f = f as ManySortedFunction of the carrier' of S by FUNCOP_1:def_6;
for i being set st i in the carrier' of S holds
f . i is Function of ((((OSClass R) #) * the Arity of S) . i),(((OSClass R) * the ResultSort of S) . i)
proof
let i be set ; ::_thesis: ( i in the carrier' of S implies f . i is Function of ((((OSClass R) #) * the Arity of S) . i),(((OSClass R) * the ResultSort of S) . i) )
assume i in the carrier' of S ; ::_thesis: f . i is Function of ((((OSClass R) #) * the Arity of S) . i),(((OSClass R) * the ResultSort of S) . i)
then reconsider i1 = i as OperSymbol of S ;
f . i1 = OSQuotCharact (R,i1) by A2;
hence f . i is Function of ((((OSClass R) #) * the Arity of S) . i),(((OSClass R) * the ResultSort of S) . i) ; ::_thesis: verum
end;
then reconsider f = f as ManySortedFunction of ((OSClass R) #) * the Arity of S,(OSClass R) * the ResultSort of S by PBOOLE:def_15;
take f ; ::_thesis: for o being OperSymbol of S holds f . o = OSQuotCharact (R,o)
thus for o being OperSymbol of S holds f . o = OSQuotCharact (R,o) by A2; ::_thesis: verum
end;
uniqueness
for b1, b2 being ManySortedFunction of ((OSClass R) #) * the Arity of S,(OSClass R) * the ResultSort of S st ( for o being OperSymbol of S holds b1 . o = OSQuotCharact (R,o) ) & ( for o being OperSymbol of S holds b2 . o = OSQuotCharact (R,o) ) holds
b1 = b2
proof
let f, g be ManySortedFunction of ((OSClass R) #) * the Arity of S,(OSClass R) * the ResultSort of S; ::_thesis: ( ( for o being OperSymbol of S holds f . o = OSQuotCharact (R,o) ) & ( for o being OperSymbol of S holds g . o = OSQuotCharact (R,o) ) implies f = g )
assume that
A3: for o being OperSymbol of S holds f . o = OSQuotCharact (R,o) and
A4: for o being OperSymbol of S holds g . o = OSQuotCharact (R,o) ; ::_thesis: f = g
now__::_thesis:_for_i_being_set_st_i_in_the_carrier'_of_S_holds_
f_._i_=_g_._i
let i be set ; ::_thesis: ( i in the carrier' of S implies f . i = g . i )
assume i in the carrier' of S ; ::_thesis: f . i = g . i
then reconsider i1 = i as OperSymbol of S ;
f . i1 = OSQuotCharact (R,i1) by A3;
hence f . i = g . i by A4; ::_thesis: verum
end;
hence f = g by PBOOLE:3; ::_thesis: verum
end;
end;
:: deftheorem Def19 defines OSQuotCharact OSALG_4:def_19_:_
for S being locally_directed OrderSortedSign
for A being non-empty OSAlgebra of S
for R being OSCongruence of A
for b4 being ManySortedFunction of ((OSClass R) #) * the Arity of S,(OSClass R) * the ResultSort of S holds
( b4 = OSQuotCharact R iff for o being OperSymbol of S holds b4 . o = OSQuotCharact (R,o) );
definition
let S be locally_directed OrderSortedSign;
let U1 be non-empty OSAlgebra of S;
let R be OSCongruence of U1;
func QuotOSAlg (U1,R) -> OSAlgebra of S equals :: OSALG_4:def 20
MSAlgebra(# (OSClass R),(OSQuotCharact R) #);
coherence
MSAlgebra(# (OSClass R),(OSQuotCharact R) #) is OSAlgebra of S by OSALG_1:17;
end;
:: deftheorem defines QuotOSAlg OSALG_4:def_20_:_
for S being locally_directed OrderSortedSign
for U1 being non-empty OSAlgebra of S
for R being OSCongruence of U1 holds QuotOSAlg (U1,R) = MSAlgebra(# (OSClass R),(OSQuotCharact R) #);
registration
let S be locally_directed OrderSortedSign;
let U1 be non-empty OSAlgebra of S;
let R be OSCongruence of U1;
cluster QuotOSAlg (U1,R) -> strict non-empty ;
coherence
( QuotOSAlg (U1,R) is strict & QuotOSAlg (U1,R) is non-empty ) by MSUALG_1:def_3;
end;
definition
let S be locally_directed OrderSortedSign;
let U1 be non-empty OSAlgebra of S;
let R be OSCongruence of U1;
let s be Element of S;
func OSNat_Hom (U1,R,s) -> Function of ( the Sorts of U1 . s),(OSClass (R,s)) means :Def21: :: OSALG_4:def 21
for x being Element of the Sorts of U1 . s holds it . x = OSClass (R,x);
existence
ex b1 being Function of ( the Sorts of U1 . s),(OSClass (R,s)) st
for x being Element of the Sorts of U1 . s holds b1 . x = OSClass (R,x)
proof
deffunc H1( Element of the Sorts of U1 . s) -> Element of OSClass (R,s) = OSClass (R,$1);
thus ex F being Function of ( the Sorts of U1 . s),(OSClass (R,s)) st
for x being Element of the Sorts of U1 . s holds F . x = H1(x) from FUNCT_2:sch_4(); ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of ( the Sorts of U1 . s),(OSClass (R,s)) st ( for x being Element of the Sorts of U1 . s holds b1 . x = OSClass (R,x) ) & ( for x being Element of the Sorts of U1 . s holds b2 . x = OSClass (R,x) ) holds
b1 = b2
proof
let f, g be Function of ( the Sorts of U1 . s),(OSClass (R,s)); ::_thesis: ( ( for x being Element of the Sorts of U1 . s holds f . x = OSClass (R,x) ) & ( for x being Element of the Sorts of U1 . s holds g . x = OSClass (R,x) ) implies f = g )
assume that
A1: for x being Element of the Sorts of U1 . s holds f . x = OSClass (R,x) and
A2: for x being Element of the Sorts of U1 . s holds g . x = OSClass (R,x) ; ::_thesis: f = g
A3: now__::_thesis:_for_x_being_set_st_x_in_the_Sorts_of_U1_._s_holds_
f_._x_=_g_._x
let x be set ; ::_thesis: ( x in the Sorts of U1 . s implies f . x = g . x )
assume x in the Sorts of U1 . s ; ::_thesis: f . x = g . x
then reconsider x1 = x as Element of the Sorts of U1 . s ;
f . x = OSClass (R,x1) by A1;
hence f . x = g . x by A2; ::_thesis: verum
end;
( dom f = the Sorts of U1 . s & dom g = the Sorts of U1 . s ) by FUNCT_2:def_1;
hence f = g by A3, FUNCT_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def21 defines OSNat_Hom OSALG_4:def_21_:_
for S being locally_directed OrderSortedSign
for U1 being non-empty OSAlgebra of S
for R being OSCongruence of U1
for s being Element of S
for b5 being Function of ( the Sorts of U1 . s),(OSClass (R,s)) holds
( b5 = OSNat_Hom (U1,R,s) iff for x being Element of the Sorts of U1 . s holds b5 . x = OSClass (R,x) );
definition
let S be locally_directed OrderSortedSign;
let U1 be non-empty OSAlgebra of S;
let R be OSCongruence of U1;
func OSNat_Hom (U1,R) -> ManySortedFunction of U1,(QuotOSAlg (U1,R)) means :Def22: :: OSALG_4:def 22
for s being Element of S holds it . s = OSNat_Hom (U1,R,s);
existence
ex b1 being ManySortedFunction of U1,(QuotOSAlg (U1,R)) st
for s being Element of S holds b1 . s = OSNat_Hom (U1,R,s)
proof
deffunc H1( Element of S) -> Function of ( the Sorts of U1 . $1),(OSClass (R,$1)) = OSNat_Hom (U1,R,$1);
consider f being Function such that
A1: ( dom f = the carrier of S & ( for d being Element of S holds f . d = H1(d) ) ) from FUNCT_1:sch_4();
reconsider f = f as ManySortedSet of the carrier of S by A1, PARTFUN1:def_2, RELAT_1:def_18;
for x being set st x in dom f holds
f . x is Function
proof
let x be set ; ::_thesis: ( x in dom f implies f . x is Function )
assume x in dom f ; ::_thesis: f . x is Function
then reconsider y = x as Element of S ;
f . y = OSNat_Hom (U1,R,y) by A1;
hence f . x is Function ; ::_thesis: verum
end;
then reconsider f = f as ManySortedFunction of the carrier of S by FUNCOP_1:def_6;
for i being set st i in the carrier of S holds
f . i is Function of ( the Sorts of U1 . i),((OSClass R) . i)
proof
let i be set ; ::_thesis: ( i in the carrier of S implies f . i is Function of ( the Sorts of U1 . i),((OSClass R) . i) )
assume i in the carrier of S ; ::_thesis: f . i is Function of ( the Sorts of U1 . i),((OSClass R) . i)
then reconsider s = i as Element of S ;
( OSClass (R,s) = (OSClass R) . i & f . s = OSNat_Hom (U1,R,s) ) by A1, Def11;
hence f . i is Function of ( the Sorts of U1 . i),((OSClass R) . i) ; ::_thesis: verum
end;
then reconsider f = f as ManySortedFunction of the Sorts of U1, OSClass R by PBOOLE:def_15;
reconsider f = f as ManySortedFunction of U1,(QuotOSAlg (U1,R)) ;
take f ; ::_thesis: for s being Element of S holds f . s = OSNat_Hom (U1,R,s)
thus for s being Element of S holds f . s = OSNat_Hom (U1,R,s) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being ManySortedFunction of U1,(QuotOSAlg (U1,R)) st ( for s being Element of S holds b1 . s = OSNat_Hom (U1,R,s) ) & ( for s being Element of S holds b2 . s = OSNat_Hom (U1,R,s) ) holds
b1 = b2
proof
let F, G be ManySortedFunction of U1,(QuotOSAlg (U1,R)); ::_thesis: ( ( for s being Element of S holds F . s = OSNat_Hom (U1,R,s) ) & ( for s being Element of S holds G . s = OSNat_Hom (U1,R,s) ) implies F = G )
assume that
A2: for s being Element of S holds F . s = OSNat_Hom (U1,R,s) and
A3: for s being Element of S holds G . s = OSNat_Hom (U1,R,s) ; ::_thesis: F = G
now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_S_holds_
F_._i_=_G_._i
let i be set ; ::_thesis: ( i in the carrier of S implies F . i = G . i )
assume i in the carrier of S ; ::_thesis: F . i = G . i
then reconsider s = i as SortSymbol of S ;
F . s = OSNat_Hom (U1,R,s) by A2;
hence F . i = G . i by A3; ::_thesis: verum
end;
hence F = G by PBOOLE:3; ::_thesis: verum
end;
end;
:: deftheorem Def22 defines OSNat_Hom OSALG_4:def_22_:_
for S being locally_directed OrderSortedSign
for U1 being non-empty OSAlgebra of S
for R being OSCongruence of U1
for b4 being ManySortedFunction of U1,(QuotOSAlg (U1,R)) holds
( b4 = OSNat_Hom (U1,R) iff for s being Element of S holds b4 . s = OSNat_Hom (U1,R,s) );
theorem :: OSALG_4:15
for S being locally_directed OrderSortedSign
for U1 being non-empty OSAlgebra of S
for R being OSCongruence of U1 holds
( OSNat_Hom (U1,R) is_epimorphism U1, QuotOSAlg (U1,R) & OSNat_Hom (U1,R) is order-sorted )
proof
let S be locally_directed OrderSortedSign; ::_thesis: for U1 being non-empty OSAlgebra of S
for R being OSCongruence of U1 holds
( OSNat_Hom (U1,R) is_epimorphism U1, QuotOSAlg (U1,R) & OSNat_Hom (U1,R) is order-sorted )
let U1 be non-empty OSAlgebra of S; ::_thesis: for R being OSCongruence of U1 holds
( OSNat_Hom (U1,R) is_epimorphism U1, QuotOSAlg (U1,R) & OSNat_Hom (U1,R) is order-sorted )
let R be OSCongruence of U1; ::_thesis: ( OSNat_Hom (U1,R) is_epimorphism U1, QuotOSAlg (U1,R) & OSNat_Hom (U1,R) is order-sorted )
set F = OSNat_Hom (U1,R);
set QA = QuotOSAlg (U1,R);
set S1 = the Sorts of U1;
for o being Element of the carrier' of S st Args (o,U1) <> {} holds
for x being Element of Args (o,U1) holds ((OSNat_Hom (U1,R)) . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,(QuotOSAlg (U1,R)))) . ((OSNat_Hom (U1,R)) # x)
proof
let o be Element of the carrier' of S; ::_thesis: ( Args (o,U1) <> {} implies for x being Element of Args (o,U1) holds ((OSNat_Hom (U1,R)) . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,(QuotOSAlg (U1,R)))) . ((OSNat_Hom (U1,R)) # x) )
assume Args (o,U1) <> {} ; ::_thesis: for x being Element of Args (o,U1) holds ((OSNat_Hom (U1,R)) . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,(QuotOSAlg (U1,R)))) . ((OSNat_Hom (U1,R)) # x)
let x be Element of Args (o,U1); ::_thesis: ((OSNat_Hom (U1,R)) . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,(QuotOSAlg (U1,R)))) . ((OSNat_Hom (U1,R)) # x)
set ro = the_result_sort_of o;
set ar = the_arity_of o;
the Arity of S . o = the_arity_of o by MSUALG_1:def_1;
then A1: (((OSClass R) #) * the Arity of S) . o = product ((OSClass R) * (the_arity_of o)) by MSAFREE:1;
A2: dom x = dom (the_arity_of o) by MSUALG_3:6;
A3: for a being set st a in dom (the_arity_of o) holds
((OSNat_Hom (U1,R)) # x) . a = (R #_os x) . a
proof
let a be set ; ::_thesis: ( a in dom (the_arity_of o) implies ((OSNat_Hom (U1,R)) # x) . a = (R #_os x) . a )
assume A4: a in dom (the_arity_of o) ; ::_thesis: ((OSNat_Hom (U1,R)) # x) . a = (R #_os x) . a
then reconsider n = a as Nat ;
set Fo = OSNat_Hom (U1,R,((the_arity_of o) /. n));
set s = (the_arity_of o) /. n;
A5: ex z being Element of the Sorts of U1 . ((the_arity_of o) /. n) st
( z = x . n & (R #_os x) . n = OSClass (R,z) ) by A4, Def13;
A6: n in dom ( the Sorts of U1 * (the_arity_of o)) by A4, PARTFUN1:def_2;
then ( the Sorts of U1 * (the_arity_of o)) . n = the Sorts of U1 . ((the_arity_of o) . n) by FUNCT_1:12
.= the Sorts of U1 . ((the_arity_of o) /. n) by A4, PARTFUN1:def_6 ;
then reconsider xn = x . n as Element of the Sorts of U1 . ((the_arity_of o) /. n) by A6, MSUALG_3:6;
thus ((OSNat_Hom (U1,R)) # x) . a = ((OSNat_Hom (U1,R)) . ((the_arity_of o) /. n)) . (x . n) by A2, A4, MSUALG_3:def_6
.= (OSNat_Hom (U1,R,((the_arity_of o) /. n))) . xn by Def22
.= (R #_os x) . a by A5, Def21 ; ::_thesis: verum
end;
dom the Sorts of U1 = the carrier of S by PARTFUN1:def_2;
then rng the ResultSort of S c= dom the Sorts of U1 ;
then ( dom the ResultSort of S = the carrier' of S & dom ( the Sorts of U1 * the ResultSort of S) = dom the ResultSort of S ) by FUNCT_2:def_1, RELAT_1:27;
then A7: ( the Sorts of U1 * the ResultSort of S) . o = the Sorts of U1 . ( the ResultSort of S . o) by FUNCT_1:12
.= the Sorts of U1 . (the_result_sort_of o) by MSUALG_1:def_2 ;
then reconsider dx = (Den (o,U1)) . x as Element of the Sorts of U1 . (the_result_sort_of o) by MSUALG_1:def_5;
( rng (Den (o,U1)) c= Result (o,U1) & Result (o,U1) = the Sorts of U1 . (the_result_sort_of o) ) by A7, MSUALG_1:def_5;
then rng (Den (o,U1)) c= dom (OSQuotRes (R,o)) by A7, FUNCT_2:def_1;
then A8: ( dom (Den (o,U1)) = Args (o,U1) & dom ((OSQuotRes (R,o)) * (Den (o,U1))) = dom (Den (o,U1)) ) by FUNCT_2:def_1, RELAT_1:27;
dom (OSClass R) = the carrier of S by PARTFUN1:def_2;
then ( dom (R #_os x) = dom ((OSClass R) * (the_arity_of o)) & rng (the_arity_of o) c= dom (OSClass R) ) by CARD_3:9;
then ( dom ((OSNat_Hom (U1,R)) # x) = dom (the_arity_of o) & dom (R #_os x) = dom (the_arity_of o) ) by MSUALG_3:6, RELAT_1:27;
then A9: (OSNat_Hom (U1,R)) # x = R #_os x by A3, FUNCT_1:2;
Den (o,(QuotOSAlg (U1,R))) = (OSQuotCharact R) . o by MSUALG_1:def_6
.= OSQuotCharact (R,o) by Def19 ;
then (Den (o,(QuotOSAlg (U1,R)))) . ((OSNat_Hom (U1,R)) # x) = ((OSQuotRes (R,o)) * (Den (o,U1))) . x by A1, A9, Def18
.= (OSQuotRes (R,o)) . dx by A8, FUNCT_1:12
.= OSClass (R,dx) by Def14
.= (OSNat_Hom (U1,R,(the_result_sort_of o))) . dx by Def21
.= ((OSNat_Hom (U1,R)) . (the_result_sort_of o)) . ((Den (o,U1)) . x) by Def22 ;
hence ((OSNat_Hom (U1,R)) . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,(QuotOSAlg (U1,R)))) . ((OSNat_Hom (U1,R)) # x) ; ::_thesis: verum
end;
hence OSNat_Hom (U1,R) is_homomorphism U1, QuotOSAlg (U1,R) by MSUALG_3:def_7; :: according to MSUALG_3:def_8 ::_thesis: ( OSNat_Hom (U1,R) is "onto" & OSNat_Hom (U1,R) is order-sorted )
for i being set st i in the carrier of S holds
rng ((OSNat_Hom (U1,R)) . i) = the Sorts of (QuotOSAlg (U1,R)) . i
proof
let i be set ; ::_thesis: ( i in the carrier of S implies rng ((OSNat_Hom (U1,R)) . i) = the Sorts of (QuotOSAlg (U1,R)) . i )
assume i in the carrier of S ; ::_thesis: rng ((OSNat_Hom (U1,R)) . i) = the Sorts of (QuotOSAlg (U1,R)) . i
then reconsider s = i as Element of S ;
reconsider f = (OSNat_Hom (U1,R)) . i as Function of ( the Sorts of U1 . s),( the Sorts of (QuotOSAlg (U1,R)) . s) by PBOOLE:def_15;
A10: dom f = the Sorts of U1 . s by FUNCT_2:def_1;
A11: the Sorts of (QuotOSAlg (U1,R)) . s = OSClass (R,s) by Def11;
for x being set st x in the Sorts of (QuotOSAlg (U1,R)) . i holds
x in rng f
proof
let x be set ; ::_thesis: ( x in the Sorts of (QuotOSAlg (U1,R)) . i implies x in rng f )
A12: f = OSNat_Hom (U1,R,s) by Def22;
assume x in the Sorts of (QuotOSAlg (U1,R)) . i ; ::_thesis: x in rng f
then consider a1 being set such that
A13: a1 in the Sorts of U1 . s and
A14: x = Class ((CompClass (R,(CComp s))),a1) by A11, Def10;
reconsider a2 = a1 as Element of the Sorts of U1 . s by A13;
( OSClass (R,a2) = x & f . a1 in rng f ) by A10, A13, A14, FUNCT_1:def_3;
hence x in rng f by A12, Def21; ::_thesis: verum
end;
then the Sorts of (QuotOSAlg (U1,R)) . i c= rng f by TARSKI:def_3;
hence rng ((OSNat_Hom (U1,R)) . i) = the Sorts of (QuotOSAlg (U1,R)) . i by XBOOLE_0:def_10; ::_thesis: verum
end;
hence OSNat_Hom (U1,R) is "onto" by MSUALG_3:def_3; ::_thesis: OSNat_Hom (U1,R) is order-sorted
thus OSNat_Hom (U1,R) is order-sorted ::_thesis: verum
proof
reconsider S2 = the Sorts of U1 as OrderSortedSet of S by OSALG_1:17;
let s1, s2 be Element of S; :: according to OSALG_3:def_1 ::_thesis: ( not s1 <= s2 or for b1 being set holds
( not b1 in dom ((OSNat_Hom (U1,R)) . s1) or ( b1 in dom ((OSNat_Hom (U1,R)) . s2) & ((OSNat_Hom (U1,R)) . s1) . b1 = ((OSNat_Hom (U1,R)) . s2) . b1 ) ) )
assume A15: s1 <= s2 ; ::_thesis: for b1 being set holds
( not b1 in dom ((OSNat_Hom (U1,R)) . s1) or ( b1 in dom ((OSNat_Hom (U1,R)) . s2) & ((OSNat_Hom (U1,R)) . s1) . b1 = ((OSNat_Hom (U1,R)) . s2) . b1 ) )
A16: S2 . s1 c= S2 . s2 by A15, OSALG_1:def_16;
let a1 be set ; ::_thesis: ( not a1 in dom ((OSNat_Hom (U1,R)) . s1) or ( a1 in dom ((OSNat_Hom (U1,R)) . s2) & ((OSNat_Hom (U1,R)) . s1) . a1 = ((OSNat_Hom (U1,R)) . s2) . a1 ) )
assume A17: a1 in dom ((OSNat_Hom (U1,R)) . s1) ; ::_thesis: ( a1 in dom ((OSNat_Hom (U1,R)) . s2) & ((OSNat_Hom (U1,R)) . s1) . a1 = ((OSNat_Hom (U1,R)) . s2) . a1 )
A18: a1 in the Sorts of U1 . s1 by A17;
then reconsider b2 = a1 as Element of the Sorts of U1 . s2 by A16;
dom ((OSNat_Hom (U1,R)) . s2) = the Sorts of U1 . s2 by FUNCT_2:def_1;
hence a1 in dom ((OSNat_Hom (U1,R)) . s2) by A16, A18; ::_thesis: ((OSNat_Hom (U1,R)) . s1) . a1 = ((OSNat_Hom (U1,R)) . s2) . a1
reconsider b1 = a1 as Element of the Sorts of U1 . s1 by A17;
thus ((OSNat_Hom (U1,R)) . s1) . a1 = (OSNat_Hom (U1,R,s1)) . b1 by Def22
.= OSClass (R,b1) by Def21
.= OSClass (R,b2) by A15, Th4
.= (OSNat_Hom (U1,R,s2)) . b2 by Def21
.= ((OSNat_Hom (U1,R)) . s2) . a1 by Def22 ; ::_thesis: verum
end;
end;
theorem Th16: :: OSALG_4:16
for S being locally_directed OrderSortedSign
for U1, U2 being non-empty OSAlgebra of S
for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 & F is order-sorted holds
MSCng F is OSCongruence of U1
proof
let S be locally_directed OrderSortedSign; ::_thesis: for U1, U2 being non-empty OSAlgebra of S
for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 & F is order-sorted holds
MSCng F is OSCongruence of U1
let U1, U2 be non-empty OSAlgebra of S; ::_thesis: for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 & F is order-sorted holds
MSCng F is OSCongruence of U1
let F be ManySortedFunction of U1,U2; ::_thesis: ( F is_homomorphism U1,U2 & F is order-sorted implies MSCng F is OSCongruence of U1 )
assume that
A1: F is_homomorphism U1,U2 and
A2: F is order-sorted ; ::_thesis: MSCng F is OSCongruence of U1
reconsider S1 = the Sorts of U1 as OrderSortedSet of S by OSALG_1:17;
MSCng F is os-compatible
proof
let s1, s2 be Element of S; :: according to OSALG_4:def_1 ::_thesis: ( s1 <= s2 implies for x, y being set st x in the Sorts of U1 . s1 & y in the Sorts of U1 . s1 holds
( [x,y] in (MSCng F) . s1 iff [x,y] in (MSCng F) . s2 ) )
assume A3: s1 <= s2 ; ::_thesis: for x, y being set st x in the Sorts of U1 . s1 & y in the Sorts of U1 . s1 holds
( [x,y] in (MSCng F) . s1 iff [x,y] in (MSCng F) . s2 )
reconsider s3 = s1, s4 = s2 as SortSymbol of S ;
let x, y be set ; ::_thesis: ( x in the Sorts of U1 . s1 & y in the Sorts of U1 . s1 implies ( [x,y] in (MSCng F) . s1 iff [x,y] in (MSCng F) . s2 ) )
assume A4: ( x in the Sorts of U1 . s1 & y in the Sorts of U1 . s1 ) ; ::_thesis: ( [x,y] in (MSCng F) . s1 iff [x,y] in (MSCng F) . s2 )
reconsider x1 = x, y1 = y as Element of the Sorts of U1 . s1 by A4;
S1 . s3 c= S1 . s4 by A3, OSALG_1:def_16;
then reconsider x2 = x, y2 = y as Element of the Sorts of U1 . s2 by A4;
A5: ( [x2,y2] in MSCng (F,s2) iff (F . s2) . x2 = (F . s2) . y2 ) by MSUALG_4:def_17;
dom (F . s3) = S1 . s3 by FUNCT_2:def_1;
then A6: ( (F . s3) . x1 = (F . s4) . x1 & (F . s3) . y1 = (F . s4) . y1 ) by A2, A3, OSALG_3:def_1;
(MSCng F) . s1 = MSCng (F,s1) by A1, MSUALG_4:def_18;
hence ( [x,y] in (MSCng F) . s1 iff [x,y] in (MSCng F) . s2 ) by A1, A5, A6, MSUALG_4:def_17, MSUALG_4:def_18; ::_thesis: verum
end;
hence MSCng F is OSCongruence of U1 by Def2; ::_thesis: verum
end;
definition
let S be locally_directed OrderSortedSign;
let U1, U2 be non-empty OSAlgebra of S;
let F be ManySortedFunction of U1,U2;
assume A1: ( F is_homomorphism U1,U2 & F is order-sorted ) ;
func OSCng F -> OSCongruence of U1 equals :Def23: :: OSALG_4:def 23
MSCng F;
correctness
coherence
MSCng F is OSCongruence of U1;
by A1, Th16;
end;
:: deftheorem Def23 defines OSCng OSALG_4:def_23_:_
for S being locally_directed OrderSortedSign
for U1, U2 being non-empty OSAlgebra of S
for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 & F is order-sorted holds
OSCng F = MSCng F;
definition
let S be locally_directed OrderSortedSign;
let U1, U2 be non-empty OSAlgebra of S;
let F be ManySortedFunction of U1,U2;
let s be Element of S;
assume that
A1: F is_homomorphism U1,U2 and
A2: F is order-sorted ;
func OSHomQuot (F,s) -> Function of ( the Sorts of (QuotOSAlg (U1,(OSCng F))) . s),( the Sorts of U2 . s) means :Def24: :: OSALG_4:def 24
for x being Element of the Sorts of U1 . s holds it . (OSClass ((OSCng F),x)) = (F . s) . x;
existence
ex b1 being Function of ( the Sorts of (QuotOSAlg (U1,(OSCng F))) . s),( the Sorts of U2 . s) st
for x being Element of the Sorts of U1 . s holds b1 . (OSClass ((OSCng F),x)) = (F . s) . x
proof
set qa = QuotOSAlg (U1,(OSCng F));
set cqa = the Sorts of (QuotOSAlg (U1,(OSCng F)));
set S1 = the Sorts of U1;
set S2 = the Sorts of U2;
defpred S1[ set , set ] means for a being Element of the Sorts of U1 . s st $1 = OSClass ((OSCng F),a) holds
$2 = (F . s) . a;
A3: the Sorts of (QuotOSAlg (U1,(OSCng F))) . s = OSClass ((OSCng F),s) by Def11;
A4: for x being set st x in the Sorts of (QuotOSAlg (U1,(OSCng F))) . s holds
ex y being set st
( y in the Sorts of U2 . s & S1[x,y] )
proof
let x be set ; ::_thesis: ( x in the Sorts of (QuotOSAlg (U1,(OSCng F))) . s implies ex y being set st
( y in the Sorts of U2 . s & S1[x,y] ) )
assume x in the Sorts of (QuotOSAlg (U1,(OSCng F))) . s ; ::_thesis: ex y being set st
( y in the Sorts of U2 . s & S1[x,y] )
then consider a being set such that
A5: a in the Sorts of U1 . s and
A6: x = Class ((CompClass ((OSCng F),(CComp s))),a) by A3, Def10;
reconsider a = a as Element of the Sorts of U1 . s by A5;
take y = (F . s) . a; ::_thesis: ( y in the Sorts of U2 . s & S1[x,y] )
thus y in the Sorts of U2 . s ; ::_thesis: S1[x,y]
let b be Element of the Sorts of U1 . s; ::_thesis: ( x = OSClass ((OSCng F),b) implies y = (F . s) . b )
assume A7: x = OSClass ((OSCng F),b) ; ::_thesis: y = (F . s) . b
x = OSClass ((OSCng F),a) by A6;
then [b,a] in (OSCng F) . s by A7, Th12;
then [b,a] in (MSCng F) . s by A1, A2, Def23;
then [b,a] in MSCng (F,s) by A1, MSUALG_4:def_18;
hence y = (F . s) . b by MSUALG_4:def_17; ::_thesis: verum
end;
consider G being Function such that
A8: ( dom G = the Sorts of (QuotOSAlg (U1,(OSCng F))) . s & rng G c= the Sorts of U2 . s & ( for x being set st x in the Sorts of (QuotOSAlg (U1,(OSCng F))) . s holds
S1[x,G . x] ) ) from FUNCT_1:sch_5(A4);
reconsider G = G as Function of ( the Sorts of (QuotOSAlg (U1,(OSCng F))) . s),( the Sorts of U2 . s) by A8, FUNCT_2:def_1, RELSET_1:4;
take G ; ::_thesis: for x being Element of the Sorts of U1 . s holds G . (OSClass ((OSCng F),x)) = (F . s) . x
let a be Element of the Sorts of U1 . s; ::_thesis: G . (OSClass ((OSCng F),a)) = (F . s) . a
thus G . (OSClass ((OSCng F),a)) = (F . s) . a by A3, A8; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of ( the Sorts of (QuotOSAlg (U1,(OSCng F))) . s),( the Sorts of U2 . s) st ( for x being Element of the Sorts of U1 . s holds b1 . (OSClass ((OSCng F),x)) = (F . s) . x ) & ( for x being Element of the Sorts of U1 . s holds b2 . (OSClass ((OSCng F),x)) = (F . s) . x ) holds
b1 = b2
proof
set qa = QuotOSAlg (U1,(OSCng F));
set cqa = the Sorts of (QuotOSAlg (U1,(OSCng F)));
set u1 = the Sorts of U1;
set u2 = the Sorts of U2;
let H, G be Function of ( the Sorts of (QuotOSAlg (U1,(OSCng F))) . s),( the Sorts of U2 . s); ::_thesis: ( ( for x being Element of the Sorts of U1 . s holds H . (OSClass ((OSCng F),x)) = (F . s) . x ) & ( for x being Element of the Sorts of U1 . s holds G . (OSClass ((OSCng F),x)) = (F . s) . x ) implies H = G )
assume that
A9: for a being Element of the Sorts of U1 . s holds H . (OSClass ((OSCng F),a)) = (F . s) . a and
A10: for a being Element of the Sorts of U1 . s holds G . (OSClass ((OSCng F),a)) = (F . s) . a ; ::_thesis: H = G
A11: the Sorts of (QuotOSAlg (U1,(OSCng F))) . s = OSClass ((OSCng F),s) by Def11;
for x being set st x in the Sorts of (QuotOSAlg (U1,(OSCng F))) . s holds
H . x = G . x
proof
let x be set ; ::_thesis: ( x in the Sorts of (QuotOSAlg (U1,(OSCng F))) . s implies H . x = G . x )
assume x in the Sorts of (QuotOSAlg (U1,(OSCng F))) . s ; ::_thesis: H . x = G . x
then consider y being set such that
A12: y in the Sorts of U1 . s and
A13: x = Class ((CompClass ((OSCng F),(CComp s))),y) by A11, Def10;
reconsider y1 = y as Element of the Sorts of U1 . s by A12;
A14: OSClass ((OSCng F),y1) = x by A13;
hence H . x = (F . s) . y1 by A9
.= G . x by A10, A14 ;
::_thesis: verum
end;
hence H = G by FUNCT_2:12; ::_thesis: verum
end;
end;
:: deftheorem Def24 defines OSHomQuot OSALG_4:def_24_:_
for S being locally_directed OrderSortedSign
for U1, U2 being non-empty OSAlgebra of S
for F being ManySortedFunction of U1,U2
for s being Element of S st F is_homomorphism U1,U2 & F is order-sorted holds
for b6 being Function of ( the Sorts of (QuotOSAlg (U1,(OSCng F))) . s),( the Sorts of U2 . s) holds
( b6 = OSHomQuot (F,s) iff for x being Element of the Sorts of U1 . s holds b6 . (OSClass ((OSCng F),x)) = (F . s) . x );
definition
let S be locally_directed OrderSortedSign;
let U1, U2 be non-empty OSAlgebra of S;
let F be ManySortedFunction of U1,U2;
func OSHomQuot F -> ManySortedFunction of (QuotOSAlg (U1,(OSCng F))),U2 means :Def25: :: OSALG_4:def 25
for s being Element of S holds it . s = OSHomQuot (F,s);
existence
ex b1 being ManySortedFunction of (QuotOSAlg (U1,(OSCng F))),U2 st
for s being Element of S holds b1 . s = OSHomQuot (F,s)
proof
deffunc H1( Element of S) -> Function of ( the Sorts of (QuotOSAlg (U1,(OSCng F))) . $1),( the Sorts of U2 . $1) = OSHomQuot (F,$1);
consider f being Function such that
A1: ( dom f = the carrier of S & ( for d being Element of S holds f . d = H1(d) ) ) from FUNCT_1:sch_4();
reconsider f = f as ManySortedSet of the carrier of S by A1, PARTFUN1:def_2, RELAT_1:def_18;
for x being set st x in dom f holds
f . x is Function
proof
let x be set ; ::_thesis: ( x in dom f implies f . x is Function )
assume x in dom f ; ::_thesis: f . x is Function
then reconsider y = x as Element of S ;
f . y = OSHomQuot (F,y) by A1;
hence f . x is Function ; ::_thesis: verum
end;
then reconsider f = f as ManySortedFunction of the carrier of S by FUNCOP_1:def_6;
for i being set st i in the carrier of S holds
f . i is Function of ( the Sorts of (QuotOSAlg (U1,(OSCng F))) . i),( the Sorts of U2 . i)
proof
let i be set ; ::_thesis: ( i in the carrier of S implies f . i is Function of ( the Sorts of (QuotOSAlg (U1,(OSCng F))) . i),( the Sorts of U2 . i) )
assume i in the carrier of S ; ::_thesis: f . i is Function of ( the Sorts of (QuotOSAlg (U1,(OSCng F))) . i),( the Sorts of U2 . i)
then reconsider s = i as Element of S ;
f . s = OSHomQuot (F,s) by A1;
hence f . i is Function of ( the Sorts of (QuotOSAlg (U1,(OSCng F))) . i),( the Sorts of U2 . i) ; ::_thesis: verum
end;
then reconsider f = f as ManySortedFunction of the Sorts of (QuotOSAlg (U1,(OSCng F))), the Sorts of U2 by PBOOLE:def_15;
reconsider f = f as ManySortedFunction of (QuotOSAlg (U1,(OSCng F))),U2 ;
take f ; ::_thesis: for s being Element of S holds f . s = OSHomQuot (F,s)
thus for s being Element of S holds f . s = OSHomQuot (F,s) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being ManySortedFunction of (QuotOSAlg (U1,(OSCng F))),U2 st ( for s being Element of S holds b1 . s = OSHomQuot (F,s) ) & ( for s being Element of S holds b2 . s = OSHomQuot (F,s) ) holds
b1 = b2
proof
let H, G be ManySortedFunction of (QuotOSAlg (U1,(OSCng F))),U2; ::_thesis: ( ( for s being Element of S holds H . s = OSHomQuot (F,s) ) & ( for s being Element of S holds G . s = OSHomQuot (F,s) ) implies H = G )
assume that
A2: for s being Element of S holds H . s = OSHomQuot (F,s) and
A3: for s being Element of S holds G . s = OSHomQuot (F,s) ; ::_thesis: H = G
now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_S_holds_
H_._i_=_G_._i
let i be set ; ::_thesis: ( i in the carrier of S implies H . i = G . i )
assume i in the carrier of S ; ::_thesis: H . i = G . i
then reconsider s = i as SortSymbol of S ;
H . s = OSHomQuot (F,s) by A2;
hence H . i = G . i by A3; ::_thesis: verum
end;
hence H = G by PBOOLE:3; ::_thesis: verum
end;
end;
:: deftheorem Def25 defines OSHomQuot OSALG_4:def_25_:_
for S being locally_directed OrderSortedSign
for U1, U2 being non-empty OSAlgebra of S
for F being ManySortedFunction of U1,U2
for b5 being ManySortedFunction of (QuotOSAlg (U1,(OSCng F))),U2 holds
( b5 = OSHomQuot F iff for s being Element of S holds b5 . s = OSHomQuot (F,s) );
theorem Th17: :: OSALG_4:17
for S being locally_directed OrderSortedSign
for U1, U2 being non-empty OSAlgebra of S
for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 & F is order-sorted holds
( OSHomQuot F is_monomorphism QuotOSAlg (U1,(OSCng F)),U2 & OSHomQuot F is order-sorted )
proof
let S be locally_directed OrderSortedSign; ::_thesis: for U1, U2 being non-empty OSAlgebra of S
for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 & F is order-sorted holds
( OSHomQuot F is_monomorphism QuotOSAlg (U1,(OSCng F)),U2 & OSHomQuot F is order-sorted )
let U1, U2 be non-empty OSAlgebra of S; ::_thesis: for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 & F is order-sorted holds
( OSHomQuot F is_monomorphism QuotOSAlg (U1,(OSCng F)),U2 & OSHomQuot F is order-sorted )
let F be ManySortedFunction of U1,U2; ::_thesis: ( F is_homomorphism U1,U2 & F is order-sorted implies ( OSHomQuot F is_monomorphism QuotOSAlg (U1,(OSCng F)),U2 & OSHomQuot F is order-sorted ) )
set mc = OSCng F;
set qa = QuotOSAlg (U1,(OSCng F));
set qh = OSHomQuot F;
set S1 = the Sorts of U1;
assume that
A1: F is_homomorphism U1,U2 and
A2: F is order-sorted ; ::_thesis: ( OSHomQuot F is_monomorphism QuotOSAlg (U1,(OSCng F)),U2 & OSHomQuot F is order-sorted )
for o being Element of the carrier' of S st Args (o,(QuotOSAlg (U1,(OSCng F)))) <> {} holds
for x being Element of Args (o,(QuotOSAlg (U1,(OSCng F)))) holds ((OSHomQuot F) . (the_result_sort_of o)) . ((Den (o,(QuotOSAlg (U1,(OSCng F))))) . x) = (Den (o,U2)) . ((OSHomQuot F) # x)
proof
let o be Element of the carrier' of S; ::_thesis: ( Args (o,(QuotOSAlg (U1,(OSCng F)))) <> {} implies for x being Element of Args (o,(QuotOSAlg (U1,(OSCng F)))) holds ((OSHomQuot F) . (the_result_sort_of o)) . ((Den (o,(QuotOSAlg (U1,(OSCng F))))) . x) = (Den (o,U2)) . ((OSHomQuot F) # x) )
assume Args (o,(QuotOSAlg (U1,(OSCng F)))) <> {} ; ::_thesis: for x being Element of Args (o,(QuotOSAlg (U1,(OSCng F)))) holds ((OSHomQuot F) . (the_result_sort_of o)) . ((Den (o,(QuotOSAlg (U1,(OSCng F))))) . x) = (Den (o,U2)) . ((OSHomQuot F) # x)
let x be Element of Args (o,(QuotOSAlg (U1,(OSCng F)))); ::_thesis: ((OSHomQuot F) . (the_result_sort_of o)) . ((Den (o,(QuotOSAlg (U1,(OSCng F))))) . x) = (Den (o,U2)) . ((OSHomQuot F) # x)
reconsider o1 = o as OperSymbol of S ;
set ro = the_result_sort_of o;
set ar = the_arity_of o;
A3: dom x = dom (the_arity_of o) by MSUALG_3:6;
Args (o,(QuotOSAlg (U1,(OSCng F)))) = (((OSClass (OSCng F)) #) * the Arity of S) . o by MSUALG_1:def_4;
then consider a being Element of Args (o,U1) such that
A4: x = (OSCng F) #_os a by Th14;
A5: dom a = dom (the_arity_of o) by MSUALG_3:6;
A6: now__::_thesis:_for_y_being_set_st_y_in_dom_(the_arity_of_o)_holds_
((OSHomQuot_F)_#_x)_._y_=_(F_#_a)_._y
let y be set ; ::_thesis: ( y in dom (the_arity_of o) implies ((OSHomQuot F) # x) . y = (F # a) . y )
assume A7: y in dom (the_arity_of o) ; ::_thesis: ((OSHomQuot F) # x) . y = (F # a) . y
then reconsider n = y as Nat ;
(the_arity_of o) . n in rng (the_arity_of o) by A7, FUNCT_1:def_3;
then reconsider s = (the_arity_of o) . n as SortSymbol of S ;
A8: (the_arity_of o) /. n = (the_arity_of o) . n by A7, PARTFUN1:def_6;
then consider an being Element of the Sorts of U1 . s such that
A9: an = a . n and
A10: x . n = OSClass ((OSCng F),an) by A4, A7, Def13;
((OSHomQuot F) # x) . n = ((OSHomQuot F) . s) . (x . n) by A3, A7, A8, MSUALG_3:def_6
.= (OSHomQuot (F,s)) . (OSClass ((OSCng F),an)) by A10, Def25
.= (F . s) . an by A1, A2, Def24
.= (F # a) . n by A5, A7, A8, A9, MSUALG_3:def_6 ;
hence ((OSHomQuot F) # x) . y = (F # a) . y ; ::_thesis: verum
end;
o in the carrier' of S ;
then o in dom ( the Sorts of U1 * the ResultSort of S) by PARTFUN1:def_2;
then A11: ( the Sorts of U1 * the ResultSort of S) . o = the Sorts of U1 . ( the ResultSort of S . o) by FUNCT_1:12
.= the Sorts of U1 . (the_result_sort_of o) by MSUALG_1:def_2 ;
then ( rng (Den (o,U1)) c= Result (o,U1) & Result (o,U1) = the Sorts of U1 . (the_result_sort_of o) ) by MSUALG_1:def_5;
then rng (Den (o,U1)) c= dom (OSQuotRes ((OSCng F),o)) by A11, FUNCT_2:def_1;
then A12: ( dom (Den (o,U1)) = Args (o,U1) & dom ((OSQuotRes ((OSCng F),o)) * (Den (o,U1))) = dom (Den (o,U1)) ) by FUNCT_2:def_1, RELAT_1:27;
the_arity_of o = the Arity of S . o by MSUALG_1:def_1;
then A13: product ((OSClass (OSCng F)) * (the_arity_of o)) = (((OSClass (OSCng F)) #) * the Arity of S) . o by MSAFREE:1;
reconsider da = (Den (o,U1)) . a as Element of the Sorts of U1 . (the_result_sort_of o) by A11, MSUALG_1:def_5;
A14: (OSHomQuot F) . (the_result_sort_of o) = OSHomQuot (F,(the_result_sort_of o)) by Def25;
Den (o,(QuotOSAlg (U1,(OSCng F)))) = (OSQuotCharact (OSCng F)) . o by MSUALG_1:def_6
.= OSQuotCharact ((OSCng F),o1) by Def19 ;
then (Den (o,(QuotOSAlg (U1,(OSCng F))))) . x = ((OSQuotRes ((OSCng F),o)) * (Den (o,U1))) . a by A4, A13, Def18
.= (OSQuotRes ((OSCng F),o)) . da by A12, FUNCT_1:12
.= OSClass ((OSCng F),da) by Def14 ;
then A15: ((OSHomQuot F) . (the_result_sort_of o)) . ((Den (o,(QuotOSAlg (U1,(OSCng F))))) . x) = (F . (the_result_sort_of o)) . ((Den (o,U1)) . a) by A1, A2, A14, Def24
.= (Den (o,U2)) . (F # a) by A1, MSUALG_3:def_7 ;
( dom ((OSHomQuot F) # x) = dom (the_arity_of o) & dom (F # a) = dom (the_arity_of o) ) by MSUALG_3:6;
hence ((OSHomQuot F) . (the_result_sort_of o)) . ((Den (o,(QuotOSAlg (U1,(OSCng F))))) . x) = (Den (o,U2)) . ((OSHomQuot F) # x) by A6, A15, FUNCT_1:2; ::_thesis: verum
end;
hence OSHomQuot F is_homomorphism QuotOSAlg (U1,(OSCng F)),U2 by MSUALG_3:def_7; :: according to MSUALG_3:def_9 ::_thesis: ( OSHomQuot F is "1-1" & OSHomQuot F is order-sorted )
for i being set st i in the carrier of S holds
(OSHomQuot F) . i is one-to-one
proof
let i be set ; ::_thesis: ( i in the carrier of S implies (OSHomQuot F) . i is one-to-one )
set f = (OSHomQuot F) . i;
assume i in the carrier of S ; ::_thesis: (OSHomQuot F) . i is one-to-one
then reconsider s = i as SortSymbol of S ;
A16: (OSHomQuot F) . i = OSHomQuot (F,s) by Def25;
for x1, x2 being set st x1 in dom ((OSHomQuot F) . i) & x2 in dom ((OSHomQuot F) . i) & ((OSHomQuot F) . i) . x1 = ((OSHomQuot F) . i) . x2 holds
x1 = x2
proof
let x1, x2 be set ; ::_thesis: ( x1 in dom ((OSHomQuot F) . i) & x2 in dom ((OSHomQuot F) . i) & ((OSHomQuot F) . i) . x1 = ((OSHomQuot F) . i) . x2 implies x1 = x2 )
assume that
A17: x1 in dom ((OSHomQuot F) . i) and
A18: x2 in dom ((OSHomQuot F) . i) and
A19: ((OSHomQuot F) . i) . x1 = ((OSHomQuot F) . i) . x2 ; ::_thesis: x1 = x2
x2 in (OSClass (OSCng F)) . s by A16, A18, FUNCT_2:def_1;
then x2 in OSClass ((OSCng F),s) by Def11;
then consider a2 being set such that
A20: a2 in the Sorts of U1 . s and
A21: x2 = Class ((CompClass ((OSCng F),(CComp s))),a2) by Def10;
reconsider a2 = a2 as Element of the Sorts of U1 . s by A20;
A22: x2 = OSClass ((OSCng F),a2) by A21;
x1 in (OSClass (OSCng F)) . s by A16, A17, FUNCT_2:def_1;
then x1 in OSClass ((OSCng F),s) by Def11;
then consider a1 being set such that
A23: a1 in the Sorts of U1 . s and
A24: x1 = Class ((CompClass ((OSCng F),(CComp s))),a1) by Def10;
reconsider a1 = a1 as Element of the Sorts of U1 . s by A23;
( (F . s) . a1 = ((OSHomQuot F) . i) . (OSClass ((OSCng F),a1)) & (F . s) . a2 = ((OSHomQuot F) . i) . (OSClass ((OSCng F),a2)) ) by A1, A2, A16, Def24;
then [a1,a2] in MSCng (F,s) by A19, A24, A21, MSUALG_4:def_17;
then [a1,a2] in (MSCng F) . s by A1, MSUALG_4:def_18;
then A25: [a1,a2] in (OSCng F) . s by A1, A2, Def23;
x1 = OSClass ((OSCng F),a1) by A24;
hence x1 = x2 by A22, A25, Th12; ::_thesis: verum
end;
hence (OSHomQuot F) . i is one-to-one by FUNCT_1:def_4; ::_thesis: verum
end;
hence OSHomQuot F is "1-1" by MSUALG_3:1; ::_thesis: OSHomQuot F is order-sorted
thus OSHomQuot F is order-sorted ::_thesis: verum
proof
reconsider S1O = the Sorts of U1 as OrderSortedSet of S by OSALG_1:17;
reconsider sqa = the Sorts of (QuotOSAlg (U1,(OSCng F))) as OrderSortedSet of S ;
let s1, s2 be Element of S; :: according to OSALG_3:def_1 ::_thesis: ( not s1 <= s2 or for b1 being set holds
( not b1 in dom ((OSHomQuot F) . s1) or ( b1 in dom ((OSHomQuot F) . s2) & ((OSHomQuot F) . s1) . b1 = ((OSHomQuot F) . s2) . b1 ) ) )
assume A26: s1 <= s2 ; ::_thesis: for b1 being set holds
( not b1 in dom ((OSHomQuot F) . s1) or ( b1 in dom ((OSHomQuot F) . s2) & ((OSHomQuot F) . s1) . b1 = ((OSHomQuot F) . s2) . b1 ) )
let a1 be set ; ::_thesis: ( not a1 in dom ((OSHomQuot F) . s1) or ( a1 in dom ((OSHomQuot F) . s2) & ((OSHomQuot F) . s1) . a1 = ((OSHomQuot F) . s2) . a1 ) )
assume A27: a1 in dom ((OSHomQuot F) . s1) ; ::_thesis: ( a1 in dom ((OSHomQuot F) . s2) & ((OSHomQuot F) . s1) . a1 = ((OSHomQuot F) . s2) . a1 )
a1 in (OSClass (OSCng F)) . s1 by A27;
then a1 in OSClass ((OSCng F),s1) by Def11;
then consider x being set such that
A28: x in the Sorts of U1 . s1 and
A29: a1 = Class ((CompClass ((OSCng F),(CComp s1))),x) by Def10;
S1O . s1 c= S1O . s2 by A26, OSALG_1:def_16;
then reconsider x2 = x as Element of the Sorts of U1 . s2 by A28;
A30: a1 = OSClass ((OSCng F),x2) by A26, A29, Th4;
reconsider s3 = s1, s4 = s2 as Element of S ;
A31: ( dom ((OSHomQuot F) . s1) = the Sorts of (QuotOSAlg (U1,(OSCng F))) . s1 & dom ((OSHomQuot F) . s2) = the Sorts of (QuotOSAlg (U1,(OSCng F))) . s2 ) by FUNCT_2:def_1;
reconsider x1 = x as Element of the Sorts of U1 . s1 by A28;
x1 in dom (F . s3) by A28, FUNCT_2:def_1;
then A32: (F . s3) . x1 = (F . s4) . x1 by A2, A26, OSALG_3:def_1;
sqa . s1 c= sqa . s2 by A26, OSALG_1:def_16;
hence a1 in dom ((OSHomQuot F) . s2) by A27, A31; ::_thesis: ((OSHomQuot F) . s1) . a1 = ((OSHomQuot F) . s2) . a1
thus ((OSHomQuot F) . s1) . a1 = (OSHomQuot (F,s1)) . (OSClass ((OSCng F),x1)) by A29, Def25
.= (F . s2) . x1 by A1, A2, A32, Def24
.= (OSHomQuot (F,s2)) . (OSClass ((OSCng F),x2)) by A1, A2, Def24
.= ((OSHomQuot F) . s2) . a1 by A30, Def25 ; ::_thesis: verum
end;
end;
theorem Th18: :: OSALG_4:18
for S being locally_directed OrderSortedSign
for U1, U2 being non-empty OSAlgebra of S
for F being ManySortedFunction of U1,U2 st F is_epimorphism U1,U2 & F is order-sorted holds
OSHomQuot F is_isomorphism QuotOSAlg (U1,(OSCng F)),U2
proof
let S be locally_directed OrderSortedSign; ::_thesis: for U1, U2 being non-empty OSAlgebra of S
for F being ManySortedFunction of U1,U2 st F is_epimorphism U1,U2 & F is order-sorted holds
OSHomQuot F is_isomorphism QuotOSAlg (U1,(OSCng F)),U2
let U1, U2 be non-empty OSAlgebra of S; ::_thesis: for F being ManySortedFunction of U1,U2 st F is_epimorphism U1,U2 & F is order-sorted holds
OSHomQuot F is_isomorphism QuotOSAlg (U1,(OSCng F)),U2
let F be ManySortedFunction of U1,U2; ::_thesis: ( F is_epimorphism U1,U2 & F is order-sorted implies OSHomQuot F is_isomorphism QuotOSAlg (U1,(OSCng F)),U2 )
set mc = OSCng F;
set qa = QuotOSAlg (U1,(OSCng F));
set qh = OSHomQuot F;
assume that
A1: F is_epimorphism U1,U2 and
A2: F is order-sorted ; ::_thesis: OSHomQuot F is_isomorphism QuotOSAlg (U1,(OSCng F)),U2
set Sq = the Sorts of (QuotOSAlg (U1,(OSCng F)));
set S1 = the Sorts of U1;
set S2 = the Sorts of U2;
A3: F is_homomorphism U1,U2 by A1, MSUALG_3:def_8;
A4: F is "onto" by A1, MSUALG_3:def_8;
for i being set st i in the carrier of S holds
rng ((OSHomQuot F) . i) = the Sorts of U2 . i
proof
let i be set ; ::_thesis: ( i in the carrier of S implies rng ((OSHomQuot F) . i) = the Sorts of U2 . i )
set f = (OSHomQuot F) . i;
assume i in the carrier of S ; ::_thesis: rng ((OSHomQuot F) . i) = the Sorts of U2 . i
then reconsider s = i as SortSymbol of S ;
A5: rng (F . s) = the Sorts of U2 . s by A4, MSUALG_3:def_3;
A6: (OSHomQuot F) . i = OSHomQuot (F,s) by Def25;
then A7: dom ((OSHomQuot F) . i) = the Sorts of (QuotOSAlg (U1,(OSCng F))) . s by FUNCT_2:def_1;
thus rng ((OSHomQuot F) . i) c= the Sorts of U2 . i by A6, RELAT_1:def_19; :: according to XBOOLE_0:def_10 ::_thesis: the Sorts of U2 . i c= rng ((OSHomQuot F) . i)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the Sorts of U2 . i or x in rng ((OSHomQuot F) . i) )
assume x in the Sorts of U2 . i ; ::_thesis: x in rng ((OSHomQuot F) . i)
then consider a being set such that
A8: a in dom (F . s) and
A9: (F . s) . a = x by A5, FUNCT_1:def_3;
A10: the Sorts of (QuotOSAlg (U1,(OSCng F))) . s = OSClass ((OSCng F),s) by Def11;
reconsider a = a as Element of the Sorts of U1 . s by A8;
((OSHomQuot F) . i) . (OSClass ((OSCng F),a)) = x by A2, A3, A6, A9, Def24;
hence x in rng ((OSHomQuot F) . i) by A7, A10, FUNCT_1:def_3; ::_thesis: verum
end;
then A11: OSHomQuot F is "onto" by MSUALG_3:def_3;
OSHomQuot F is_monomorphism QuotOSAlg (U1,(OSCng F)),U2 by A2, A3, Th17;
then ( OSHomQuot F is_homomorphism QuotOSAlg (U1,(OSCng F)),U2 & OSHomQuot F is "1-1" ) by MSUALG_3:def_9;
hence OSHomQuot F is_isomorphism QuotOSAlg (U1,(OSCng F)),U2 by A11, MSUALG_3:13; ::_thesis: verum
end;
theorem :: OSALG_4:19
for S being locally_directed OrderSortedSign
for U1, U2 being non-empty OSAlgebra of S
for F being ManySortedFunction of U1,U2 st F is_epimorphism U1,U2 & F is order-sorted holds
QuotOSAlg (U1,(OSCng F)),U2 are_isomorphic
proof
let S be locally_directed OrderSortedSign; ::_thesis: for U1, U2 being non-empty OSAlgebra of S
for F being ManySortedFunction of U1,U2 st F is_epimorphism U1,U2 & F is order-sorted holds
QuotOSAlg (U1,(OSCng F)),U2 are_isomorphic
let U1, U2 be non-empty OSAlgebra of S; ::_thesis: for F being ManySortedFunction of U1,U2 st F is_epimorphism U1,U2 & F is order-sorted holds
QuotOSAlg (U1,(OSCng F)),U2 are_isomorphic
let F be ManySortedFunction of U1,U2; ::_thesis: ( F is_epimorphism U1,U2 & F is order-sorted implies QuotOSAlg (U1,(OSCng F)),U2 are_isomorphic )
assume ( F is_epimorphism U1,U2 & F is order-sorted ) ; ::_thesis: QuotOSAlg (U1,(OSCng F)),U2 are_isomorphic
then OSHomQuot F is_isomorphism QuotOSAlg (U1,(OSCng F)),U2 by Th18;
hence QuotOSAlg (U1,(OSCng F)),U2 are_isomorphic by MSUALG_3:def_11; ::_thesis: verum
end;
definition
let S be OrderSortedSign;
let U1 be non-empty OSAlgebra of S;
let R be MSEquivalence-like OrderSortedRelation of U1;
attrR is monotone means :Def26: :: OSALG_4:def 26
for o1, o2 being OperSymbol of S st o1 <= o2 holds
for x1 being Element of Args (o1,U1)
for x2 being Element of Args (o2,U1) st ( for y being Nat st y in dom x1 holds
[(x1 . y),(x2 . y)] in R . ((the_arity_of o2) /. y) ) holds
[((Den (o1,U1)) . x1),((Den (o2,U1)) . x2)] in R . (the_result_sort_of o2);
end;
:: deftheorem Def26 defines monotone OSALG_4:def_26_:_
for S being OrderSortedSign
for U1 being non-empty OSAlgebra of S
for R being MSEquivalence-like OrderSortedRelation of U1 holds
( R is monotone iff for o1, o2 being OperSymbol of S st o1 <= o2 holds
for x1 being Element of Args (o1,U1)
for x2 being Element of Args (o2,U1) st ( for y being Nat st y in dom x1 holds
[(x1 . y),(x2 . y)] in R . ((the_arity_of o2) /. y) ) holds
[((Den (o1,U1)) . x1),((Den (o2,U1)) . x2)] in R . (the_result_sort_of o2) );
theorem Th20: :: OSALG_4:20
for S being OrderSortedSign
for U1 being non-empty OSAlgebra of S holds [| the Sorts of U1, the Sorts of U1|] is OSCongruence of U1
proof
let S be OrderSortedSign; ::_thesis: for U1 being non-empty OSAlgebra of S holds [| the Sorts of U1, the Sorts of U1|] is OSCongruence of U1
let U1 be non-empty OSAlgebra of S; ::_thesis: [| the Sorts of U1, the Sorts of U1|] is OSCongruence of U1
reconsider C = [| the Sorts of U1, the Sorts of U1|] as MSCongruence of U1 by MSUALG_5:18;
C is os-compatible
proof
reconsider O1 = the Sorts of U1 as OrderSortedSet of S by OSALG_1:17;
let s1, s2 be Element of S; :: according to OSALG_4:def_1 ::_thesis: ( s1 <= s2 implies for x, y being set st x in the Sorts of U1 . s1 & y in the Sorts of U1 . s1 holds
( [x,y] in C . s1 iff [x,y] in C . s2 ) )
assume A1: s1 <= s2 ; ::_thesis: for x, y being set st x in the Sorts of U1 . s1 & y in the Sorts of U1 . s1 holds
( [x,y] in C . s1 iff [x,y] in C . s2 )
reconsider s3 = s1, s4 = s2 as Element of S ;
A2: O1 . s3 c= O1 . s4 by A1, OSALG_1:def_16;
A3: ( C . s1 = [:( the Sorts of U1 . s1),( the Sorts of U1 . s1):] & C . s2 = [:( the Sorts of U1 . s2),( the Sorts of U1 . s2):] ) by PBOOLE:def_16;
let x, y be set ; ::_thesis: ( x in the Sorts of U1 . s1 & y in the Sorts of U1 . s1 implies ( [x,y] in C . s1 iff [x,y] in C . s2 ) )
assume ( x in the Sorts of U1 . s1 & y in the Sorts of U1 . s1 ) ; ::_thesis: ( [x,y] in C . s1 iff [x,y] in C . s2 )
hence ( [x,y] in C . s1 iff [x,y] in C . s2 ) by A2, A3, ZFMISC_1:87; ::_thesis: verum
end;
hence [| the Sorts of U1, the Sorts of U1|] is OSCongruence of U1 by Def2; ::_thesis: verum
end;
theorem Th21: :: OSALG_4:21
for S being OrderSortedSign
for U1 being non-empty OSAlgebra of S
for R being OSCongruence of U1 st R = [| the Sorts of U1, the Sorts of U1|] holds
R is monotone
proof
let S be OrderSortedSign; ::_thesis: for U1 being non-empty OSAlgebra of S
for R being OSCongruence of U1 st R = [| the Sorts of U1, the Sorts of U1|] holds
R is monotone
let U1 be non-empty OSAlgebra of S; ::_thesis: for R being OSCongruence of U1 st R = [| the Sorts of U1, the Sorts of U1|] holds
R is monotone
let R be OSCongruence of U1; ::_thesis: ( R = [| the Sorts of U1, the Sorts of U1|] implies R is monotone )
assume A1: R = [| the Sorts of U1, the Sorts of U1|] ; ::_thesis: R is monotone
reconsider O1 = the Sorts of U1 as OrderSortedSet of S by OSALG_1:17;
let o1, o2 be OperSymbol of S; :: according to OSALG_4:def_26 ::_thesis: ( o1 <= o2 implies for x1 being Element of Args (o1,U1)
for x2 being Element of Args (o2,U1) st ( for y being Nat st y in dom x1 holds
[(x1 . y),(x2 . y)] in R . ((the_arity_of o2) /. y) ) holds
[((Den (o1,U1)) . x1),((Den (o2,U1)) . x2)] in R . (the_result_sort_of o2) )
assume A2: o1 <= o2 ; ::_thesis: for x1 being Element of Args (o1,U1)
for x2 being Element of Args (o2,U1) st ( for y being Nat st y in dom x1 holds
[(x1 . y),(x2 . y)] in R . ((the_arity_of o2) /. y) ) holds
[((Den (o1,U1)) . x1),((Den (o2,U1)) . x2)] in R . (the_result_sort_of o2)
set s2 = the_result_sort_of o2;
set s1 = the_result_sort_of o1;
the_result_sort_of o1 <= the_result_sort_of o2 by A2, OSALG_1:def_20;
then A3: O1 . (the_result_sort_of o1) c= O1 . (the_result_sort_of o2) by OSALG_1:def_16;
let x1 be Element of Args (o1,U1); ::_thesis: for x2 being Element of Args (o2,U1) st ( for y being Nat st y in dom x1 holds
[(x1 . y),(x2 . y)] in R . ((the_arity_of o2) /. y) ) holds
[((Den (o1,U1)) . x1),((Den (o2,U1)) . x2)] in R . (the_result_sort_of o2)
let x2 be Element of Args (o2,U1); ::_thesis: ( ( for y being Nat st y in dom x1 holds
[(x1 . y),(x2 . y)] in R . ((the_arity_of o2) /. y) ) implies [((Den (o1,U1)) . x1),((Den (o2,U1)) . x2)] in R . (the_result_sort_of o2) )
assume for y being Nat st y in dom x1 holds
[(x1 . y),(x2 . y)] in R . ((the_arity_of o2) /. y) ; ::_thesis: [((Den (o1,U1)) . x1),((Den (o2,U1)) . x2)] in R . (the_result_sort_of o2)
A4: ( (Den (o1,U1)) . x1 in the Sorts of U1 . (the_result_sort_of o1) & (Den (o2,U1)) . x2 in the Sorts of U1 . (the_result_sort_of o2) ) by MSUALG_9:18;
R . (the_result_sort_of o2) = [:( the Sorts of U1 . (the_result_sort_of o2)),( the Sorts of U1 . (the_result_sort_of o2)):] by A1, PBOOLE:def_16;
hence [((Den (o1,U1)) . x1),((Den (o2,U1)) . x2)] in R . (the_result_sort_of o2) by A3, A4, ZFMISC_1:87; ::_thesis: verum
end;
registration
let S be OrderSortedSign;
let U1 be non-empty OSAlgebra of S;
cluster non empty Relation-like the carrier of S -defined Function-like total Relation-yielding MSEquivalence-like MSCongruence-like monotone for OrderSortedRelation of U1;
existence
ex b1 being OSCongruence of U1 st b1 is monotone
proof
reconsider R = [| the Sorts of U1, the Sorts of U1|] as OSCongruence of U1 by Th20;
take R ; ::_thesis: R is monotone
thus R is monotone by Th21; ::_thesis: verum
end;
end;
registration
let S be OrderSortedSign;
let U1 be non-empty OSAlgebra of S;
cluster non empty Relation-like the carrier of S -defined Function-like total Relation-yielding MSEquivalence-like monotone for OrderSortedRelation of U1;
existence
ex b1 being MSEquivalence-like OrderSortedRelation of U1 st b1 is monotone
proof
set R = the monotone OSCongruence of U1;
take the monotone OSCongruence of U1 ; ::_thesis: the monotone OSCongruence of U1 is monotone
thus the monotone OSCongruence of U1 is monotone ; ::_thesis: verum
end;
end;
theorem Th22: :: OSALG_4:22
for S being OrderSortedSign
for U1 being non-empty OSAlgebra of S
for R being MSEquivalence-like monotone OrderSortedRelation of U1 holds R is MSCongruence-like
proof
let S be OrderSortedSign; ::_thesis: for U1 being non-empty OSAlgebra of S
for R being MSEquivalence-like monotone OrderSortedRelation of U1 holds R is MSCongruence-like
let U1 be non-empty OSAlgebra of S; ::_thesis: for R being MSEquivalence-like monotone OrderSortedRelation of U1 holds R is MSCongruence-like
let R be MSEquivalence-like monotone OrderSortedRelation of U1; ::_thesis: R is MSCongruence-like
for o being Element of the carrier' of S
for x, y being Element of Args (o,U1) st ( for n being Nat st n in dom x holds
[(x . n),(y . n)] in R . ((the_arity_of o) /. n) ) holds
[((Den (o,U1)) . x),((Den (o,U1)) . y)] in R . (the_result_sort_of o) by Def26;
hence R is MSCongruence-like by MSUALG_4:def_4; ::_thesis: verum
end;
registration
let S be OrderSortedSign;
let U1 be non-empty OSAlgebra of S;
cluster MSEquivalence-like monotone -> MSEquivalence-like MSCongruence-like for OrderSortedRelation of U1;
coherence
for b1 being MSEquivalence-like OrderSortedRelation of U1 st b1 is monotone holds
b1 is MSCongruence-like by Th22;
end;
theorem Th23: :: OSALG_4:23
for S being OrderSortedSign
for U1 being non-empty monotone OSAlgebra of S
for R being OSCongruence of U1 holds R is monotone
proof
let S be OrderSortedSign; ::_thesis: for U1 being non-empty monotone OSAlgebra of S
for R being OSCongruence of U1 holds R is monotone
let U1 be non-empty monotone OSAlgebra of S; ::_thesis: for R being OSCongruence of U1 holds R is monotone
let R be OSCongruence of U1; ::_thesis: R is monotone
let o1, o2 be OperSymbol of S; :: according to OSALG_4:def_26 ::_thesis: ( o1 <= o2 implies for x1 being Element of Args (o1,U1)
for x2 being Element of Args (o2,U1) st ( for y being Nat st y in dom x1 holds
[(x1 . y),(x2 . y)] in R . ((the_arity_of o2) /. y) ) holds
[((Den (o1,U1)) . x1),((Den (o2,U1)) . x2)] in R . (the_result_sort_of o2) )
assume A1: o1 <= o2 ; ::_thesis: for x1 being Element of Args (o1,U1)
for x2 being Element of Args (o2,U1) st ( for y being Nat st y in dom x1 holds
[(x1 . y),(x2 . y)] in R . ((the_arity_of o2) /. y) ) holds
[((Den (o1,U1)) . x1),((Den (o2,U1)) . x2)] in R . (the_result_sort_of o2)
let x1 be Element of Args (o1,U1); ::_thesis: for x2 being Element of Args (o2,U1) st ( for y being Nat st y in dom x1 holds
[(x1 . y),(x2 . y)] in R . ((the_arity_of o2) /. y) ) holds
[((Den (o1,U1)) . x1),((Den (o2,U1)) . x2)] in R . (the_result_sort_of o2)
Args (o1,U1) c= Args (o2,U1) by A1, OSALG_1:26;
then reconsider x3 = x1 as Element of Args (o2,U1) by TARSKI:def_3;
let x2 be Element of Args (o2,U1); ::_thesis: ( ( for y being Nat st y in dom x1 holds
[(x1 . y),(x2 . y)] in R . ((the_arity_of o2) /. y) ) implies [((Den (o1,U1)) . x1),((Den (o2,U1)) . x2)] in R . (the_result_sort_of o2) )
assume for y being Nat st y in dom x1 holds
[(x1 . y),(x2 . y)] in R . ((the_arity_of o2) /. y) ; ::_thesis: [((Den (o1,U1)) . x1),((Den (o2,U1)) . x2)] in R . (the_result_sort_of o2)
then A2: [((Den (o2,U1)) . x3),((Den (o2,U1)) . x2)] in R . (the_result_sort_of o2) by MSUALG_4:def_4;
x1 in Args (o1,U1) ;
then A3: x1 in dom (Den (o1,U1)) by FUNCT_2:def_1;
Den (o1,U1) c= Den (o2,U1) by A1, OSALG_1:27;
hence [((Den (o1,U1)) . x1),((Den (o2,U1)) . x2)] in R . (the_result_sort_of o2) by A2, A3, GRFUNC_1:2; ::_thesis: verum
end;
registration
let S be OrderSortedSign;
let U1 be non-empty monotone OSAlgebra of S;
cluster MSEquivalence-like MSCongruence-like -> monotone for OrderSortedRelation of U1;
coherence
for b1 being OSCongruence of U1 holds b1 is monotone by Th23;
end;
registration
let S be locally_directed OrderSortedSign;
let U1 be non-empty OSAlgebra of S;
let R be monotone OSCongruence of U1;
cluster QuotOSAlg (U1,R) -> monotone ;
coherence
QuotOSAlg (U1,R) is monotone
proof
reconsider O1 = the Sorts of U1 as OrderSortedSet of S by OSALG_1:17;
set A = QuotOSAlg (U1,R);
let o1, o2 be OperSymbol of S; :: according to OSALG_1:def_21 ::_thesis: ( not o1 <= o2 or (Den (o2,(QuotOSAlg (U1,R)))) | (Args (o1,(QuotOSAlg (U1,R)))) = Den (o1,(QuotOSAlg (U1,R))) )
assume A1: o1 <= o2 ; ::_thesis: (Den (o2,(QuotOSAlg (U1,R)))) | (Args (o1,(QuotOSAlg (U1,R)))) = Den (o1,(QuotOSAlg (U1,R)))
A2: Args (o1,(QuotOSAlg (U1,R))) c= Args (o2,(QuotOSAlg (U1,R))) by A1, OSALG_1:26;
Den (o2,(QuotOSAlg (U1,R))) = (OSQuotCharact R) . o2 by MSUALG_1:def_6;
then A3: Den (o2,(QuotOSAlg (U1,R))) = OSQuotCharact (R,o2) by Def19;
o2 in the carrier' of S ;
then A4: o2 in dom the ResultSort of S by FUNCT_2:def_1;
Den (o1,(QuotOSAlg (U1,R))) = (OSQuotCharact R) . o1 by MSUALG_1:def_6;
then A5: Den (o1,(QuotOSAlg (U1,R))) = OSQuotCharact (R,o1) by Def19;
o1 in the carrier' of S ;
then A6: o1 in dom the ResultSort of S by FUNCT_2:def_1;
A7: the_arity_of o1 <= the_arity_of o2 by A1, OSALG_1:def_20;
then len (the_arity_of o1) = len (the_arity_of o2) by OSALG_1:def_6;
then A8: dom (the_arity_of o1) = dom (the_arity_of o2) by FINSEQ_3:29;
A9: the_result_sort_of o1 <= the_result_sort_of o2 by A1, OSALG_1:def_20;
then A10: O1 . (the_result_sort_of o1) c= O1 . (the_result_sort_of o2) by OSALG_1:def_17;
A11: for x being set st x in dom (Den (o1,(QuotOSAlg (U1,R)))) holds
(Den (o1,(QuotOSAlg (U1,R)))) . x = (Den (o2,(QuotOSAlg (U1,R)))) . x
proof
let x be set ; ::_thesis: ( x in dom (Den (o1,(QuotOSAlg (U1,R)))) implies (Den (o1,(QuotOSAlg (U1,R)))) . x = (Den (o2,(QuotOSAlg (U1,R)))) . x )
assume x in dom (Den (o1,(QuotOSAlg (U1,R)))) ; ::_thesis: (Den (o1,(QuotOSAlg (U1,R)))) . x = (Den (o2,(QuotOSAlg (U1,R)))) . x
then A12: x in Args (o1,(QuotOSAlg (U1,R))) ;
then A13: x in (((OSClass R) #) * the Arity of S) . o1 by MSUALG_1:def_4;
then consider a1 being Element of Args (o1,U1) such that
A14: x = R #_os a1 by Th14;
Result (o1,U1) = ( the Sorts of U1 * the ResultSort of S) . o1 by MSUALG_1:def_5
.= the Sorts of U1 . ( the ResultSort of S . o1) by A6, FUNCT_1:13
.= the Sorts of U1 . (the_result_sort_of o1) by MSUALG_1:def_2 ;
then reconsider da1 = (Den (o1,U1)) . a1 as Element of the Sorts of U1 . (the_result_sort_of o1) ;
reconsider da12 = da1 as Element of the Sorts of U1 . (the_result_sort_of o2) by A10, TARSKI:def_3;
a1 in Args (o1,U1) ;
then a1 in dom (Den (o1,U1)) by FUNCT_2:def_1;
then A15: ((OSQuotRes (R,o1)) * (Den (o1,U1))) . a1 = (OSQuotRes (R,o1)) . da1 by FUNCT_1:13
.= OSClass (R,da1) by Def14 ;
A16: (OSQuotCharact (R,o1)) . (R #_os a1) = ((OSQuotRes (R,o1)) * (Den (o1,U1))) . a1 by A13, A14, Def18;
x in Args (o2,(QuotOSAlg (U1,R))) by A2, A12;
then A17: x in (((OSClass R) #) * the Arity of S) . o2 by MSUALG_1:def_4;
then consider a2 being Element of Args (o2,U1) such that
A18: x = R #_os a2 by Th14;
for y being Nat st y in dom a1 holds
[(a1 . y),(a2 . y)] in R . ((the_arity_of o2) /. y)
proof
let y be Nat; ::_thesis: ( y in dom a1 implies [(a1 . y),(a2 . y)] in R . ((the_arity_of o2) /. y) )
assume A19: y in dom a1 ; ::_thesis: [(a1 . y),(a2 . y)] in R . ((the_arity_of o2) /. y)
A20: y in dom (the_arity_of o1) by A19, MSUALG_6:2;
then consider z1 being Element of the Sorts of U1 . ((the_arity_of o1) /. y) such that
A21: z1 = a1 . y and
A22: (R #_os a1) . y = OSClass (R,z1) by Def13;
reconsider s1 = (the_arity_of o1) . y, s2 = (the_arity_of o2) . y as SortSymbol of S by A8, A20, PARTFUN1:4;
A23: y in dom (the_arity_of o2) by A8, A19, MSUALG_6:2;
then A24: (the_arity_of o2) /. y = (the_arity_of o2) . y by PARTFUN1:def_6;
A25: ( (the_arity_of o1) /. y = (the_arity_of o1) . y & s1 <= s2 ) by A7, A20, OSALG_1:def_6, PARTFUN1:def_6;
then the Sorts of U1 . ((the_arity_of o1) /. y) c= the Sorts of U1 . ((the_arity_of o2) /. y) by A24, OSALG_1:def_17;
then reconsider z12 = z1 as Element of the Sorts of U1 . ((the_arity_of o2) /. y) by TARSKI:def_3;
consider z2 being Element of the Sorts of U1 . ((the_arity_of o2) /. y) such that
A26: z2 = a2 . y and
A27: (R #_os a2) . y = OSClass (R,z2) by A23, Def13;
OSClass (R,z2) = OSClass (R,z12) by A14, A18, A22, A27, A24, A25, Th4;
hence [(a1 . y),(a2 . y)] in R . ((the_arity_of o2) /. y) by A21, A26, Th12; ::_thesis: verum
end;
then A28: [((Den (o1,U1)) . a1),((Den (o2,U1)) . a2)] in R . (the_result_sort_of o2) by A1, Def26;
Result (o2,U1) = ( the Sorts of U1 * the ResultSort of S) . o2 by MSUALG_1:def_5
.= the Sorts of U1 . ( the ResultSort of S . o2) by A4, FUNCT_1:13
.= the Sorts of U1 . (the_result_sort_of o2) by MSUALG_1:def_2 ;
then reconsider da2 = (Den (o2,U1)) . a2 as Element of the Sorts of U1 . (the_result_sort_of o2) ;
a2 in Args (o2,U1) ;
then a2 in dom (Den (o2,U1)) by FUNCT_2:def_1;
then A29: ((OSQuotRes (R,o2)) * (Den (o2,U1))) . a2 = (OSQuotRes (R,o2)) . da2 by FUNCT_1:13
.= OSClass (R,da2) by Def14 ;
OSClass (R,da1) = OSClass (R,da12) by A9, Th4
.= OSClass (R,da2) by A28, Th12 ;
hence (Den (o1,(QuotOSAlg (U1,R)))) . x = (Den (o2,(QuotOSAlg (U1,R)))) . x by A5, A3, A17, A14, A18, A16, A15, A29, Def18; ::_thesis: verum
end;
( dom (Den (o2,(QuotOSAlg (U1,R)))) = Args (o2,(QuotOSAlg (U1,R))) & dom (Den (o1,(QuotOSAlg (U1,R)))) = Args (o1,(QuotOSAlg (U1,R))) ) by FUNCT_2:def_1;
then dom (Den (o1,(QuotOSAlg (U1,R)))) = (dom (Den (o2,(QuotOSAlg (U1,R))))) /\ (Args (o1,(QuotOSAlg (U1,R)))) by A2, XBOOLE_1:28;
hence (Den (o2,(QuotOSAlg (U1,R)))) | (Args (o1,(QuotOSAlg (U1,R)))) = Den (o1,(QuotOSAlg (U1,R))) by A11, FUNCT_1:46; ::_thesis: verum
end;
end;
theorem :: OSALG_4:24
for S being locally_directed OrderSortedSign
for U1 being non-empty OSAlgebra of S
for U2 being non-empty monotone OSAlgebra of S
for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 & F is order-sorted holds
OSCng F is monotone
proof
let S be locally_directed OrderSortedSign; ::_thesis: for U1 being non-empty OSAlgebra of S
for U2 being non-empty monotone OSAlgebra of S
for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 & F is order-sorted holds
OSCng F is monotone
let U1 be non-empty OSAlgebra of S; ::_thesis: for U2 being non-empty monotone OSAlgebra of S
for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 & F is order-sorted holds
OSCng F is monotone
let U2 be non-empty monotone OSAlgebra of S; ::_thesis: for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 & F is order-sorted holds
OSCng F is monotone
let F be ManySortedFunction of U1,U2; ::_thesis: ( F is_homomorphism U1,U2 & F is order-sorted implies OSCng F is monotone )
assume that
A1: F is_homomorphism U1,U2 and
A2: F is order-sorted ; ::_thesis: OSCng F is monotone
reconsider S1 = the Sorts of U1 as OrderSortedSet of S by OSALG_1:17;
set O1 = the Sorts of U1;
let o1, o2 be OperSymbol of S; :: according to OSALG_4:def_26 ::_thesis: ( o1 <= o2 implies for x1 being Element of Args (o1,U1)
for x2 being Element of Args (o2,U1) st ( for y being Nat st y in dom x1 holds
[(x1 . y),(x2 . y)] in (OSCng F) . ((the_arity_of o2) /. y) ) holds
[((Den (o1,U1)) . x1),((Den (o2,U1)) . x2)] in (OSCng F) . (the_result_sort_of o2) )
assume A3: o1 <= o2 ; ::_thesis: for x1 being Element of Args (o1,U1)
for x2 being Element of Args (o2,U1) st ( for y being Nat st y in dom x1 holds
[(x1 . y),(x2 . y)] in (OSCng F) . ((the_arity_of o2) /. y) ) holds
[((Den (o1,U1)) . x1),((Den (o2,U1)) . x2)] in (OSCng F) . (the_result_sort_of o2)
A4: (Den (o2,U2)) | (Args (o1,U2)) = Den (o1,U2) by A3, OSALG_1:def_21;
set R = OSCng F;
set rs1 = the_result_sort_of o1;
set rs2 = the_result_sort_of o2;
let x1 be Element of Args (o1,U1); ::_thesis: for x2 being Element of Args (o2,U1) st ( for y being Nat st y in dom x1 holds
[(x1 . y),(x2 . y)] in (OSCng F) . ((the_arity_of o2) /. y) ) holds
[((Den (o1,U1)) . x1),((Den (o2,U1)) . x2)] in (OSCng F) . (the_result_sort_of o2)
let x2 be Element of Args (o2,U1); ::_thesis: ( ( for y being Nat st y in dom x1 holds
[(x1 . y),(x2 . y)] in (OSCng F) . ((the_arity_of o2) /. y) ) implies [((Den (o1,U1)) . x1),((Den (o2,U1)) . x2)] in (OSCng F) . (the_result_sort_of o2) )
assume A5: for y being Nat st y in dom x1 holds
[(x1 . y),(x2 . y)] in (OSCng F) . ((the_arity_of o2) /. y) ; ::_thesis: [((Den (o1,U1)) . x1),((Den (o2,U1)) . x2)] in (OSCng F) . (the_result_sort_of o2)
Args (o1,U1) c= Args (o2,U1) by A3, OSALG_1:26;
then reconsider x12 = x1 as Element of Args (o2,U1) by TARSKI:def_3;
set D1 = (Den (o1,U1)) . x1;
set D2 = (Den (o2,U1)) . x2;
set M = MSCng F;
A6: (Den (o1,U1)) . x1 in S1 . (the_result_sort_of o1) by MSUALG_9:18;
F # x1 in Args (o1,U2) ;
then A7: F # x1 in dom (Den (o1,U2)) by FUNCT_2:def_1;
A8: the_result_sort_of o1 <= the_result_sort_of o2 by A3, OSALG_1:def_20;
then S1 . (the_result_sort_of o1) c= S1 . (the_result_sort_of o2) by OSALG_1:def_16;
then reconsider D11 = (Den (o1,U1)) . x1, D12 = (Den (o2,U1)) . x12 as Element of the Sorts of U1 . (the_result_sort_of o2) by A6, MSUALG_9:18;
(Den (o1,U1)) . x1 in dom (F . (the_result_sort_of o1)) by A6, FUNCT_2:def_1;
then (F . (the_result_sort_of o2)) . ((Den (o1,U1)) . x1) = (F . (the_result_sort_of o1)) . ((Den (o1,U1)) . x1) by A2, A8, OSALG_3:def_1
.= (Den (o1,U2)) . (F # x1) by A1, MSUALG_3:def_7
.= (Den (o2,U2)) . (F # x1) by A7, A4, FUNCT_1:47
.= (Den (o2,U2)) . (F # x12) by A2, A3, OSALG_3:12
.= (F . (the_result_sort_of o2)) . ((Den (o2,U1)) . x12) by A1, MSUALG_3:def_7 ;
then A9: ( (Den (o2,U1)) . x2 in the Sorts of U1 . (the_result_sort_of o2) & [D11,D12] in MSCng (F,(the_result_sort_of o2)) ) by MSUALG_4:def_17, MSUALG_9:18;
field ((OSCng F) . (the_result_sort_of o2)) = the Sorts of U1 . (the_result_sort_of o2) by ORDERS_1:12;
then A10: (OSCng F) . (the_result_sort_of o2) is_transitive_in the Sorts of U1 . (the_result_sort_of o2) by RELAT_2:def_16;
A11: [((Den (o2,U1)) . x12),((Den (o2,U1)) . x2)] in (OSCng F) . (the_result_sort_of o2) by A5, MSUALG_4:def_4;
( (MSCng F) . (the_result_sort_of o2) = MSCng (F,(the_result_sort_of o2)) & MSCng F = OSCng F ) by A1, A2, Def23, MSUALG_4:def_18;
hence [((Den (o1,U1)) . x1),((Den (o2,U1)) . x2)] in (OSCng F) . (the_result_sort_of o2) by A11, A9, A10, RELAT_2:def_8; ::_thesis: verum
end;
definition
let S be locally_directed OrderSortedSign;
let U1, U2 be non-empty OSAlgebra of S;
let F be ManySortedFunction of U1,U2;
let R be OSCongruence of U1;
let s be Element of S;
assume that
A1: F is_homomorphism U1,U2 and
A2: F is order-sorted and
A3: R c= OSCng F ;
func OSHomQuot (F,R,s) -> Function of ( the Sorts of (QuotOSAlg (U1,R)) . s),( the Sorts of U2 . s) means :Def27: :: OSALG_4:def 27
for x being Element of the Sorts of U1 . s holds it . (OSClass (R,x)) = (F . s) . x;
existence
ex b1 being Function of ( the Sorts of (QuotOSAlg (U1,R)) . s),( the Sorts of U2 . s) st
for x being Element of the Sorts of U1 . s holds b1 . (OSClass (R,x)) = (F . s) . x
proof
set qa = QuotOSAlg (U1,R);
set cqa = the Sorts of (QuotOSAlg (U1,R));
set S1 = the Sorts of U1;
set S2 = the Sorts of U2;
defpred S1[ set , set ] means for a being Element of the Sorts of U1 . s st $1 = OSClass (R,a) holds
$2 = (F . s) . a;
A4: the Sorts of (QuotOSAlg (U1,R)) . s = OSClass (R,s) by Def11;
A5: for x being set st x in the Sorts of (QuotOSAlg (U1,R)) . s holds
ex y being set st
( y in the Sorts of U2 . s & S1[x,y] )
proof
let x be set ; ::_thesis: ( x in the Sorts of (QuotOSAlg (U1,R)) . s implies ex y being set st
( y in the Sorts of U2 . s & S1[x,y] ) )
A6: R . s c= (OSCng F) . s by A3, PBOOLE:def_2;
assume x in the Sorts of (QuotOSAlg (U1,R)) . s ; ::_thesis: ex y being set st
( y in the Sorts of U2 . s & S1[x,y] )
then consider a being set such that
A7: a in the Sorts of U1 . s and
A8: x = Class ((CompClass (R,(CComp s))),a) by A4, Def10;
reconsider a = a as Element of the Sorts of U1 . s by A7;
take y = (F . s) . a; ::_thesis: ( y in the Sorts of U2 . s & S1[x,y] )
thus y in the Sorts of U2 . s ; ::_thesis: S1[x,y]
let b be Element of the Sorts of U1 . s; ::_thesis: ( x = OSClass (R,b) implies y = (F . s) . b )
assume A9: x = OSClass (R,b) ; ::_thesis: y = (F . s) . b
x = OSClass (R,a) by A8;
then [b,a] in R . s by A9, Th12;
then [b,a] in (OSCng F) . s by A6;
then [b,a] in (MSCng F) . s by A1, A2, Def23;
then [b,a] in MSCng (F,s) by A1, MSUALG_4:def_18;
hence y = (F . s) . b by MSUALG_4:def_17; ::_thesis: verum
end;
consider G being Function such that
A10: ( dom G = the Sorts of (QuotOSAlg (U1,R)) . s & rng G c= the Sorts of U2 . s & ( for x being set st x in the Sorts of (QuotOSAlg (U1,R)) . s holds
S1[x,G . x] ) ) from FUNCT_1:sch_5(A5);
reconsider G = G as Function of ( the Sorts of (QuotOSAlg (U1,R)) . s),( the Sorts of U2 . s) by A10, FUNCT_2:def_1, RELSET_1:4;
take G ; ::_thesis: for x being Element of the Sorts of U1 . s holds G . (OSClass (R,x)) = (F . s) . x
let a be Element of the Sorts of U1 . s; ::_thesis: G . (OSClass (R,a)) = (F . s) . a
thus G . (OSClass (R,a)) = (F . s) . a by A4, A10; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of ( the Sorts of (QuotOSAlg (U1,R)) . s),( the Sorts of U2 . s) st ( for x being Element of the Sorts of U1 . s holds b1 . (OSClass (R,x)) = (F . s) . x ) & ( for x being Element of the Sorts of U1 . s holds b2 . (OSClass (R,x)) = (F . s) . x ) holds
b1 = b2
proof
set qa = QuotOSAlg (U1,R);
set cqa = the Sorts of (QuotOSAlg (U1,R));
set u1 = the Sorts of U1;
set u2 = the Sorts of U2;
let H, G be Function of ( the Sorts of (QuotOSAlg (U1,R)) . s),( the Sorts of U2 . s); ::_thesis: ( ( for x being Element of the Sorts of U1 . s holds H . (OSClass (R,x)) = (F . s) . x ) & ( for x being Element of the Sorts of U1 . s holds G . (OSClass (R,x)) = (F . s) . x ) implies H = G )
assume that
A11: for a being Element of the Sorts of U1 . s holds H . (OSClass (R,a)) = (F . s) . a and
A12: for a being Element of the Sorts of U1 . s holds G . (OSClass (R,a)) = (F . s) . a ; ::_thesis: H = G
A13: the Sorts of (QuotOSAlg (U1,R)) . s = OSClass (R,s) by Def11;
for x being set st x in the Sorts of (QuotOSAlg (U1,R)) . s holds
H . x = G . x
proof
let x be set ; ::_thesis: ( x in the Sorts of (QuotOSAlg (U1,R)) . s implies H . x = G . x )
assume x in the Sorts of (QuotOSAlg (U1,R)) . s ; ::_thesis: H . x = G . x
then consider y being set such that
A14: y in the Sorts of U1 . s and
A15: x = Class ((CompClass (R,(CComp s))),y) by A13, Def10;
reconsider y1 = y as Element of the Sorts of U1 . s by A14;
A16: OSClass (R,y1) = x by A15;
hence H . x = (F . s) . y1 by A11
.= G . x by A12, A16 ;
::_thesis: verum
end;
hence H = G by FUNCT_2:12; ::_thesis: verum
end;
end;
:: deftheorem Def27 defines OSHomQuot OSALG_4:def_27_:_
for S being locally_directed OrderSortedSign
for U1, U2 being non-empty OSAlgebra of S
for F being ManySortedFunction of U1,U2
for R being OSCongruence of U1
for s being Element of S st F is_homomorphism U1,U2 & F is order-sorted & R c= OSCng F holds
for b7 being Function of ( the Sorts of (QuotOSAlg (U1,R)) . s),( the Sorts of U2 . s) holds
( b7 = OSHomQuot (F,R,s) iff for x being Element of the Sorts of U1 . s holds b7 . (OSClass (R,x)) = (F . s) . x );
definition
let S be locally_directed OrderSortedSign;
let U1, U2 be non-empty OSAlgebra of S;
let F be ManySortedFunction of U1,U2;
let R be OSCongruence of U1;
func OSHomQuot (F,R) -> ManySortedFunction of (QuotOSAlg (U1,R)),U2 means :Def28: :: OSALG_4:def 28
for s being Element of S holds it . s = OSHomQuot (F,R,s);
existence
ex b1 being ManySortedFunction of (QuotOSAlg (U1,R)),U2 st
for s being Element of S holds b1 . s = OSHomQuot (F,R,s)
proof
deffunc H1( Element of S) -> Function of ( the Sorts of (QuotOSAlg (U1,R)) . $1),( the Sorts of U2 . $1) = OSHomQuot (F,R,$1);
consider f being Function such that
A1: ( dom f = the carrier of S & ( for d being Element of S holds f . d = H1(d) ) ) from FUNCT_1:sch_4();
reconsider f = f as ManySortedSet of the carrier of S by A1, PARTFUN1:def_2, RELAT_1:def_18;
for x being set st x in dom f holds
f . x is Function
proof
let x be set ; ::_thesis: ( x in dom f implies f . x is Function )
assume x in dom f ; ::_thesis: f . x is Function
then reconsider y = x as Element of S ;
f . y = OSHomQuot (F,R,y) by A1;
hence f . x is Function ; ::_thesis: verum
end;
then reconsider f = f as ManySortedFunction of the carrier of S by FUNCOP_1:def_6;
for i being set st i in the carrier of S holds
f . i is Function of ( the Sorts of (QuotOSAlg (U1,R)) . i),( the Sorts of U2 . i)
proof
let i be set ; ::_thesis: ( i in the carrier of S implies f . i is Function of ( the Sorts of (QuotOSAlg (U1,R)) . i),( the Sorts of U2 . i) )
assume i in the carrier of S ; ::_thesis: f . i is Function of ( the Sorts of (QuotOSAlg (U1,R)) . i),( the Sorts of U2 . i)
then reconsider s = i as Element of S ;
f . s = OSHomQuot (F,R,s) by A1;
hence f . i is Function of ( the Sorts of (QuotOSAlg (U1,R)) . i),( the Sorts of U2 . i) ; ::_thesis: verum
end;
then reconsider f = f as ManySortedFunction of the Sorts of (QuotOSAlg (U1,R)), the Sorts of U2 by PBOOLE:def_15;
reconsider f = f as ManySortedFunction of (QuotOSAlg (U1,R)),U2 ;
take f ; ::_thesis: for s being Element of S holds f . s = OSHomQuot (F,R,s)
thus for s being Element of S holds f . s = OSHomQuot (F,R,s) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being ManySortedFunction of (QuotOSAlg (U1,R)),U2 st ( for s being Element of S holds b1 . s = OSHomQuot (F,R,s) ) & ( for s being Element of S holds b2 . s = OSHomQuot (F,R,s) ) holds
b1 = b2
proof
let H, G be ManySortedFunction of (QuotOSAlg (U1,R)),U2; ::_thesis: ( ( for s being Element of S holds H . s = OSHomQuot (F,R,s) ) & ( for s being Element of S holds G . s = OSHomQuot (F,R,s) ) implies H = G )
assume that
A2: for s being Element of S holds H . s = OSHomQuot (F,R,s) and
A3: for s being Element of S holds G . s = OSHomQuot (F,R,s) ; ::_thesis: H = G
now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_S_holds_
H_._i_=_G_._i
let i be set ; ::_thesis: ( i in the carrier of S implies H . i = G . i )
assume i in the carrier of S ; ::_thesis: H . i = G . i
then reconsider s = i as SortSymbol of S ;
H . s = OSHomQuot (F,R,s) by A2;
hence H . i = G . i by A3; ::_thesis: verum
end;
hence H = G by PBOOLE:3; ::_thesis: verum
end;
end;
:: deftheorem Def28 defines OSHomQuot OSALG_4:def_28_:_
for S being locally_directed OrderSortedSign
for U1, U2 being non-empty OSAlgebra of S
for F being ManySortedFunction of U1,U2
for R being OSCongruence of U1
for b6 being ManySortedFunction of (QuotOSAlg (U1,R)),U2 holds
( b6 = OSHomQuot (F,R) iff for s being Element of S holds b6 . s = OSHomQuot (F,R,s) );
theorem :: OSALG_4:25
for S being locally_directed OrderSortedSign
for U1, U2 being non-empty OSAlgebra of S
for F being ManySortedFunction of U1,U2
for R being OSCongruence of U1 st F is_homomorphism U1,U2 & F is order-sorted & R c= OSCng F holds
( OSHomQuot (F,R) is_homomorphism QuotOSAlg (U1,R),U2 & OSHomQuot (F,R) is order-sorted )
proof
let S be locally_directed OrderSortedSign; ::_thesis: for U1, U2 being non-empty OSAlgebra of S
for F being ManySortedFunction of U1,U2
for R being OSCongruence of U1 st F is_homomorphism U1,U2 & F is order-sorted & R c= OSCng F holds
( OSHomQuot (F,R) is_homomorphism QuotOSAlg (U1,R),U2 & OSHomQuot (F,R) is order-sorted )
let U1, U2 be non-empty OSAlgebra of S; ::_thesis: for F being ManySortedFunction of U1,U2
for R being OSCongruence of U1 st F is_homomorphism U1,U2 & F is order-sorted & R c= OSCng F holds
( OSHomQuot (F,R) is_homomorphism QuotOSAlg (U1,R),U2 & OSHomQuot (F,R) is order-sorted )
let F be ManySortedFunction of U1,U2; ::_thesis: for R being OSCongruence of U1 st F is_homomorphism U1,U2 & F is order-sorted & R c= OSCng F holds
( OSHomQuot (F,R) is_homomorphism QuotOSAlg (U1,R),U2 & OSHomQuot (F,R) is order-sorted )
let R be OSCongruence of U1; ::_thesis: ( F is_homomorphism U1,U2 & F is order-sorted & R c= OSCng F implies ( OSHomQuot (F,R) is_homomorphism QuotOSAlg (U1,R),U2 & OSHomQuot (F,R) is order-sorted ) )
set mc = R;
set qa = QuotOSAlg (U1,R);
set qh = OSHomQuot (F,R);
set S1 = the Sorts of U1;
assume that
A1: F is_homomorphism U1,U2 and
A2: F is order-sorted and
A3: R c= OSCng F ; ::_thesis: ( OSHomQuot (F,R) is_homomorphism QuotOSAlg (U1,R),U2 & OSHomQuot (F,R) is order-sorted )
for o being Element of the carrier' of S st Args (o,(QuotOSAlg (U1,R))) <> {} holds
for x being Element of Args (o,(QuotOSAlg (U1,R))) holds ((OSHomQuot (F,R)) . (the_result_sort_of o)) . ((Den (o,(QuotOSAlg (U1,R)))) . x) = (Den (o,U2)) . ((OSHomQuot (F,R)) # x)
proof
let o be Element of the carrier' of S; ::_thesis: ( Args (o,(QuotOSAlg (U1,R))) <> {} implies for x being Element of Args (o,(QuotOSAlg (U1,R))) holds ((OSHomQuot (F,R)) . (the_result_sort_of o)) . ((Den (o,(QuotOSAlg (U1,R)))) . x) = (Den (o,U2)) . ((OSHomQuot (F,R)) # x) )
assume Args (o,(QuotOSAlg (U1,R))) <> {} ; ::_thesis: for x being Element of Args (o,(QuotOSAlg (U1,R))) holds ((OSHomQuot (F,R)) . (the_result_sort_of o)) . ((Den (o,(QuotOSAlg (U1,R)))) . x) = (Den (o,U2)) . ((OSHomQuot (F,R)) # x)
let x be Element of Args (o,(QuotOSAlg (U1,R))); ::_thesis: ((OSHomQuot (F,R)) . (the_result_sort_of o)) . ((Den (o,(QuotOSAlg (U1,R)))) . x) = (Den (o,U2)) . ((OSHomQuot (F,R)) # x)
reconsider o1 = o as OperSymbol of S ;
set ro = the_result_sort_of o;
set ar = the_arity_of o;
A4: dom x = dom (the_arity_of o) by MSUALG_3:6;
Args (o,(QuotOSAlg (U1,R))) = (((OSClass R) #) * the Arity of S) . o by MSUALG_1:def_4;
then consider a being Element of Args (o,U1) such that
A5: x = R #_os a by Th14;
A6: dom a = dom (the_arity_of o) by MSUALG_3:6;
A7: now__::_thesis:_for_y_being_set_st_y_in_dom_(the_arity_of_o)_holds_
((OSHomQuot_(F,R))_#_x)_._y_=_(F_#_a)_._y
let y be set ; ::_thesis: ( y in dom (the_arity_of o) implies ((OSHomQuot (F,R)) # x) . y = (F # a) . y )
assume A8: y in dom (the_arity_of o) ; ::_thesis: ((OSHomQuot (F,R)) # x) . y = (F # a) . y
then reconsider n = y as Nat ;
(the_arity_of o) . n in rng (the_arity_of o) by A8, FUNCT_1:def_3;
then reconsider s = (the_arity_of o) . n as SortSymbol of S ;
A9: (the_arity_of o) /. n = (the_arity_of o) . n by A8, PARTFUN1:def_6;
then consider an being Element of the Sorts of U1 . s such that
A10: an = a . n and
A11: x . n = OSClass (R,an) by A5, A8, Def13;
((OSHomQuot (F,R)) # x) . n = ((OSHomQuot (F,R)) . s) . (x . n) by A4, A8, A9, MSUALG_3:def_6
.= (OSHomQuot (F,R,s)) . (OSClass (R,an)) by A11, Def28
.= (F . s) . an by A1, A2, A3, Def27
.= (F # a) . n by A6, A8, A9, A10, MSUALG_3:def_6 ;
hence ((OSHomQuot (F,R)) # x) . y = (F # a) . y ; ::_thesis: verum
end;
o in the carrier' of S ;
then o in dom ( the Sorts of U1 * the ResultSort of S) by PARTFUN1:def_2;
then A12: ( the Sorts of U1 * the ResultSort of S) . o = the Sorts of U1 . ( the ResultSort of S . o) by FUNCT_1:12
.= the Sorts of U1 . (the_result_sort_of o) by MSUALG_1:def_2 ;
then ( rng (Den (o,U1)) c= Result (o,U1) & Result (o,U1) = the Sorts of U1 . (the_result_sort_of o) ) by MSUALG_1:def_5;
then rng (Den (o,U1)) c= dom (OSQuotRes (R,o)) by A12, FUNCT_2:def_1;
then A13: ( dom (Den (o,U1)) = Args (o,U1) & dom ((OSQuotRes (R,o)) * (Den (o,U1))) = dom (Den (o,U1)) ) by FUNCT_2:def_1, RELAT_1:27;
the_arity_of o = the Arity of S . o by MSUALG_1:def_1;
then A14: product ((OSClass R) * (the_arity_of o)) = (((OSClass R) #) * the Arity of S) . o by MSAFREE:1;
reconsider da = (Den (o,U1)) . a as Element of the Sorts of U1 . (the_result_sort_of o) by A12, MSUALG_1:def_5;
A15: (OSHomQuot (F,R)) . (the_result_sort_of o) = OSHomQuot (F,R,(the_result_sort_of o)) by Def28;
Den (o,(QuotOSAlg (U1,R))) = (OSQuotCharact R) . o by MSUALG_1:def_6
.= OSQuotCharact (R,o1) by Def19 ;
then (Den (o,(QuotOSAlg (U1,R)))) . x = ((OSQuotRes (R,o)) * (Den (o,U1))) . a by A5, A14, Def18
.= (OSQuotRes (R,o)) . da by A13, FUNCT_1:12
.= OSClass (R,da) by Def14 ;
then A16: ((OSHomQuot (F,R)) . (the_result_sort_of o)) . ((Den (o,(QuotOSAlg (U1,R)))) . x) = (F . (the_result_sort_of o)) . ((Den (o,U1)) . a) by A1, A2, A3, A15, Def27
.= (Den (o,U2)) . (F # a) by A1, MSUALG_3:def_7 ;
( dom ((OSHomQuot (F,R)) # x) = dom (the_arity_of o) & dom (F # a) = dom (the_arity_of o) ) by MSUALG_3:6;
hence ((OSHomQuot (F,R)) . (the_result_sort_of o)) . ((Den (o,(QuotOSAlg (U1,R)))) . x) = (Den (o,U2)) . ((OSHomQuot (F,R)) # x) by A7, A16, FUNCT_1:2; ::_thesis: verum
end;
hence OSHomQuot (F,R) is_homomorphism QuotOSAlg (U1,R),U2 by MSUALG_3:def_7; ::_thesis: OSHomQuot (F,R) is order-sorted
thus OSHomQuot (F,R) is order-sorted ::_thesis: verum
proof
reconsider S1O = the Sorts of U1 as OrderSortedSet of S by OSALG_1:17;
reconsider sqa = the Sorts of (QuotOSAlg (U1,R)) as OrderSortedSet of S ;
let s1, s2 be Element of S; :: according to OSALG_3:def_1 ::_thesis: ( not s1 <= s2 or for b1 being set holds
( not b1 in dom ((OSHomQuot (F,R)) . s1) or ( b1 in dom ((OSHomQuot (F,R)) . s2) & ((OSHomQuot (F,R)) . s1) . b1 = ((OSHomQuot (F,R)) . s2) . b1 ) ) )
assume A17: s1 <= s2 ; ::_thesis: for b1 being set holds
( not b1 in dom ((OSHomQuot (F,R)) . s1) or ( b1 in dom ((OSHomQuot (F,R)) . s2) & ((OSHomQuot (F,R)) . s1) . b1 = ((OSHomQuot (F,R)) . s2) . b1 ) )
let a1 be set ; ::_thesis: ( not a1 in dom ((OSHomQuot (F,R)) . s1) or ( a1 in dom ((OSHomQuot (F,R)) . s2) & ((OSHomQuot (F,R)) . s1) . a1 = ((OSHomQuot (F,R)) . s2) . a1 ) )
assume A18: a1 in dom ((OSHomQuot (F,R)) . s1) ; ::_thesis: ( a1 in dom ((OSHomQuot (F,R)) . s2) & ((OSHomQuot (F,R)) . s1) . a1 = ((OSHomQuot (F,R)) . s2) . a1 )
a1 in (OSClass R) . s1 by A18;
then a1 in OSClass (R,s1) by Def11;
then consider x being set such that
A19: x in the Sorts of U1 . s1 and
A20: a1 = Class ((CompClass (R,(CComp s1))),x) by Def10;
S1O . s1 c= S1O . s2 by A17, OSALG_1:def_16;
then reconsider x2 = x as Element of the Sorts of U1 . s2 by A19;
A21: a1 = OSClass (R,x2) by A17, A20, Th4;
reconsider s3 = s1, s4 = s2 as Element of S ;
A22: ( dom ((OSHomQuot (F,R)) . s1) = the Sorts of (QuotOSAlg (U1,R)) . s1 & dom ((OSHomQuot (F,R)) . s2) = the Sorts of (QuotOSAlg (U1,R)) . s2 ) by FUNCT_2:def_1;
reconsider x1 = x as Element of the Sorts of U1 . s1 by A19;
x1 in dom (F . s3) by A19, FUNCT_2:def_1;
then A23: (F . s3) . x1 = (F . s4) . x1 by A2, A17, OSALG_3:def_1;
sqa . s1 c= sqa . s2 by A17, OSALG_1:def_16;
hence a1 in dom ((OSHomQuot (F,R)) . s2) by A18, A22; ::_thesis: ((OSHomQuot (F,R)) . s1) . a1 = ((OSHomQuot (F,R)) . s2) . a1
thus ((OSHomQuot (F,R)) . s1) . a1 = (OSHomQuot (F,R,s1)) . (OSClass (R,x1)) by A20, Def28
.= (F . s2) . x1 by A1, A2, A3, A23, Def27
.= (OSHomQuot (F,R,s2)) . (OSClass (R,x2)) by A1, A2, A3, Def27
.= ((OSHomQuot (F,R)) . s2) . a1 by A21, Def28 ; ::_thesis: verum
end;
end;