:: MSSUBLAT semantic presentation
begin
theorem Th1: :: MSSUBLAT:1
for a being set holds (*--> a) . 0 = {}
proof
let a be set ; ::_thesis: (*--> a) . 0 = {}
thus (*--> a) . 0 = 0 |-> a by FINSEQ_2:def_6
.= {} ; ::_thesis: verum
end;
theorem :: MSSUBLAT:2
for a being set holds (*--> a) . 1 = <*a*>
proof
let a be set ; ::_thesis: (*--> a) . 1 = <*a*>
thus (*--> a) . 1 = 1 |-> a by FINSEQ_2:def_6
.= <*a*> by FINSEQ_2:59 ; ::_thesis: verum
end;
theorem :: MSSUBLAT:3
for a being set holds (*--> a) . 2 = <*a,a*>
proof
let a be set ; ::_thesis: (*--> a) . 2 = <*a,a*>
thus (*--> a) . 2 = 2 |-> a by FINSEQ_2:def_6
.= <*a,a*> by FINSEQ_2:61 ; ::_thesis: verum
end;
theorem :: MSSUBLAT:4
for a being set holds (*--> a) . 3 = <*a,a,a*>
proof
let a be set ; ::_thesis: (*--> a) . 3 = <*a,a,a*>
thus (*--> a) . 3 = 3 |-> a by FINSEQ_2:def_6
.= <*a,a,a*> by FINSEQ_2:62 ; ::_thesis: verum
end;
theorem Th5: :: MSSUBLAT:5
for i being Nat
for f being FinSequence of {0} holds
( f = i |-> 0 iff len f = i )
proof
let i be Nat; ::_thesis: for f being FinSequence of {0} holds
( f = i |-> 0 iff len f = i )
let f be FinSequence of {0}; ::_thesis: ( f = i |-> 0 iff len f = i )
thus ( f = i |-> 0 implies len f = i ) by CARD_1:def_7; ::_thesis: ( len f = i implies f = i |-> 0 )
assume len f = i ; ::_thesis: f = i |-> 0
then A1: dom f = Seg i by FINSEQ_1:def_3;
percases ( Seg i = {} or Seg i <> {} ) ;
supposeA2: Seg i = {} ; ::_thesis: f = i |-> 0
hence f = {} by A1
.= 0 |-> 0
.= i |-> 0 by A2 ;
::_thesis: verum
end;
supposeA3: Seg i <> {} ; ::_thesis: f = i |-> 0
rng f c= {0} by FINSEQ_1:def_4;
then ( rng f = {0} or rng f = {} ) by ZFMISC_1:33;
hence f = i |-> 0 by A1, A3, FUNCOP_1:9, RELAT_1:42; ::_thesis: verum
end;
end;
end;
theorem Th6: :: MSSUBLAT:6
for i being Nat
for f being FinSequence st f = (*--> 0) . i holds
len f = i
proof
let i be Nat; ::_thesis: for f being FinSequence st f = (*--> 0) . i holds
len f = i
let p be FinSequence; ::_thesis: ( p = (*--> 0) . i implies len p = i )
assume A1: p = (*--> 0) . i ; ::_thesis: len p = i
i in NAT by ORDINAL1:def_12;
then p = i |-> 0 by A1, FINSEQ_2:def_6;
hence len p = i by CARD_1:def_7; ::_thesis: verum
end;
begin
reconsider z = 0 as Element of {0} by TARSKI:def_1;
theorem Th7: :: MSSUBLAT:7
for U1, U2 being Universal_Algebra st U1 is SubAlgebra of U2 holds
MSSign U1 = MSSign U2
proof
let U1, U2 be Universal_Algebra; ::_thesis: ( U1 is SubAlgebra of U2 implies MSSign U1 = MSSign U2 )
set ff2 = (dom (signature U1)) --> z;
set gg2 = (dom (signature U2)) --> z;
reconsider ff1 = (*--> 0) * (signature U1) as Function of (dom (signature U1)),({0} *) by MSUALG_1:2;
reconsider gg1 = (*--> 0) * (signature U2) as Function of (dom (signature U2)),({0} *) by MSUALG_1:2;
assume U1 is SubAlgebra of U2 ; ::_thesis: MSSign U1 = MSSign U2
then A1: U1,U2 are_similar by UNIALG_2:13;
A2: ( MSSign U1 = ManySortedSign(# {0},(dom (signature U1)),ff1,((dom (signature U1)) --> z) #) & MSSign U2 = ManySortedSign(# {0},(dom (signature U2)),gg1,((dom (signature U2)) --> z) #) ) by MSUALG_1:10;
then the carrier' of (MSSign U1) = the carrier' of (MSSign U2) by A1, UNIALG_2:def_1;
hence MSSign U1 = MSSign U2 by A1, A2, UNIALG_2:def_1; ::_thesis: verum
end;
theorem Th8: :: MSSUBLAT:8
for U1, U2 being Universal_Algebra st U1 is SubAlgebra of U2 holds
for B being MSSubset of (MSAlg U2) st B = the Sorts of (MSAlg U1) holds
for o being OperSymbol of (MSSign U2)
for a being OperSymbol of (MSSign U1) st a = o holds
Den (a,(MSAlg U1)) = (Den (o,(MSAlg U2))) | (Args (a,(MSAlg U1)))
proof
let U1, U2 be Universal_Algebra; ::_thesis: ( U1 is SubAlgebra of U2 implies for B being MSSubset of (MSAlg U2) st B = the Sorts of (MSAlg U1) holds
for o being OperSymbol of (MSSign U2)
for a being OperSymbol of (MSSign U1) st a = o holds
Den (a,(MSAlg U1)) = (Den (o,(MSAlg U2))) | (Args (a,(MSAlg U1))) )
assume A1: U1 is SubAlgebra of U2 ; ::_thesis: for B being MSSubset of (MSAlg U2) st B = the Sorts of (MSAlg U1) holds
for o being OperSymbol of (MSSign U2)
for a being OperSymbol of (MSSign U1) st a = o holds
Den (a,(MSAlg U1)) = (Den (o,(MSAlg U2))) | (Args (a,(MSAlg U1)))
A2: MSSign U1 = MSSign U2 by A1, Th7;
A3: MSSign U1 = MSSign U2 by A1, Th7;
let B be MSSubset of (MSAlg U2); ::_thesis: ( B = the Sorts of (MSAlg U1) implies for o being OperSymbol of (MSSign U2)
for a being OperSymbol of (MSSign U1) st a = o holds
Den (a,(MSAlg U1)) = (Den (o,(MSAlg U2))) | (Args (a,(MSAlg U1))) )
assume A4: B = the Sorts of (MSAlg U1) ; ::_thesis: for o being OperSymbol of (MSSign U2)
for a being OperSymbol of (MSSign U1) st a = o holds
Den (a,(MSAlg U1)) = (Den (o,(MSAlg U2))) | (Args (a,(MSAlg U1)))
let o be OperSymbol of (MSSign U2); ::_thesis: for a being OperSymbol of (MSSign U1) st a = o holds
Den (a,(MSAlg U1)) = (Den (o,(MSAlg U2))) | (Args (a,(MSAlg U1)))
reconsider a = o as Element of the carrier' of (MSSign U1) by A1, Th7;
set X = Args (a,(MSAlg U1));
set Y = dom (Den (a,(MSAlg U1)));
( the Sorts of (MSAlg U2) is MSSubset of (MSAlg U2) & B c= the Sorts of (MSAlg U2) ) by PBOOLE:def_18;
then A5: ((B #) * the Arity of (MSSign U1)) . a c= (( the Sorts of (MSAlg U2) #) * the Arity of (MSSign U2)) . o by A3, MSUALG_2:2;
( dom (Den (o,(MSAlg U2))) = Args (o,(MSAlg U2)) & Args (o,(MSAlg U2)) = (( the Sorts of (MSAlg U2) #) * the Arity of (MSSign U2)) . o ) by FUNCT_2:def_1, MSUALG_1:def_4;
then Args (a,(MSAlg U1)) c= dom (Den (o,(MSAlg U2))) by A4, A2, A5, MSUALG_1:def_4;
then dom ((Den (o,(MSAlg U2))) | (Args (a,(MSAlg U1)))) = Args (a,(MSAlg U1)) by RELAT_1:62;
then dom ((Den (o,(MSAlg U2))) | (Args (a,(MSAlg U1)))) = dom (Den (a,(MSAlg U1))) by FUNCT_2:def_1;
then A6: dom (Den (a,(MSAlg U1))) = (dom (Den (o,(MSAlg U2)))) /\ (Args (a,(MSAlg U1))) by RELAT_1:61;
for x being set st x in dom (Den (a,(MSAlg U1))) holds
(Den (o,(MSAlg U2))) . x = (Den (a,(MSAlg U1))) . x
proof
MSAlg U1 = MSAlgebra(# (MSSorts U1),(MSCharact U1) #) by MSUALG_1:def_11;
then the Sorts of (MSAlg U1) = 0 .--> the carrier of U1 by MSUALG_1:def_9;
then rng the Sorts of (MSAlg U1) = { the carrier of U1} by FUNCOP_1:8;
then A7: the carrier of U1 is Component of the Sorts of (MSAlg U1) by TARSKI:def_1;
reconsider cc = the carrier of U1 as non empty Subset of U2 by A1, UNIALG_2:def_7;
let x be set ; ::_thesis: ( x in dom (Den (a,(MSAlg U1))) implies (Den (o,(MSAlg U2))) . x = (Den (a,(MSAlg U1))) . x )
A8: MSAlg U2 = MSAlgebra(# (MSSorts U2),(MSCharact U2) #) by MSUALG_1:def_11;
U1,U2 are_similar by A1, UNIALG_2:13;
then A9: signature U1 = signature U2 by UNIALG_2:def_1;
assume x in dom (Den (a,(MSAlg U1))) ; ::_thesis: (Den (o,(MSAlg U2))) . x = (Den (a,(MSAlg U1))) . x
then x in Args (a,(MSAlg U1)) by A6, XBOOLE_0:def_4;
then x in (len (the_arity_of a)) -tuples_on (the_sort_of (MSAlg U1)) by MSUALG_1:6;
then A10: x in (len (the_arity_of a)) -tuples_on the carrier of U1 by A7, MSUALG_1:def_12;
reconsider gg1 = (*--> 0) * (signature U2) as Function of (dom (signature U2)),({0} *) by MSUALG_1:2;
set ff1 = (*--> 0) * (signature U1);
set ff2 = (dom (signature U1)) --> z;
set gg2 = (dom (signature U2)) --> z;
reconsider ff1 = (*--> 0) * (signature U1) as Function of (dom (signature U1)),({0} *) by MSUALG_1:2;
consider n being Nat such that
A11: dom (signature U2) = Seg n by FINSEQ_1:def_2;
A12: MSSign U2 = ManySortedSign(# {0},(dom (signature U2)),gg1,((dom (signature U2)) --> z) #) by MSUALG_1:10;
then A13: a in Seg n by A11;
A14: dom the charact of U2 = Seg (len the charact of U2) by FINSEQ_1:def_3
.= Seg (len (signature U2)) by UNIALG_1:def_4
.= dom (signature U2) by FINSEQ_1:def_3 ;
then reconsider op = the charact of U2 . a as operation of U2 by A12, FUNCT_1:def_3;
reconsider a = a as Element of NAT by A13;
A15: rng (signature U1) c= NAT by FINSEQ_1:def_4;
U1,U2 are_similar by A1, UNIALG_2:13;
then A16: signature U1 = signature U2 by UNIALG_2:def_1;
then A17: (signature U1) . a in rng (signature U1) by A12, FUNCT_1:def_3;
then reconsider sig = (signature U1) . a as Element of NAT by A15;
dom (*--> 0) = NAT by FUNCT_2:def_1;
then ( MSSign U1 = ManySortedSign(# {0},(dom (signature U1)),ff1,((dom (signature U1)) --> z) #) & a in dom ((*--> 0) * (signature U1)) ) by A12, A16, A17, A15, FUNCT_1:11, MSUALG_1:10;
then the Arity of (MSSign U1) . a = (*--> 0) . ((signature U1) . a) by FUNCT_1:12;
then A18: the Arity of (MSSign U1) . a = sig |-> 0 by FINSEQ_2:def_6;
reconsider ar = the Arity of (MSSign U1) . a as FinSequence ;
x in (len ar) -tuples_on the carrier of U1 by A10, MSUALG_1:def_1;
then x in sig -tuples_on the carrier of U1 by A18, CARD_1:def_7;
then A19: x in (arity op) -tuples_on the carrier of U1 by A12, A9, UNIALG_1:def_4;
now__::_thesis:_for_n_being_set_st_n_in_dom_(Opers_(U2,cc))_holds_
(Opers_(U2,cc))_._n_is_Function
let n be set ; ::_thesis: ( n in dom (Opers (U2,cc)) implies (Opers (U2,cc)) . n is Function )
assume n in dom (Opers (U2,cc)) ; ::_thesis: (Opers (U2,cc)) . n is Function
then ( rng (Opers (U2,cc)) c= PFuncs ((cc *),cc) & (Opers (U2,cc)) . n in rng (Opers (U2,cc)) ) by FINSEQ_1:def_4, FUNCT_1:def_3;
hence (Opers (U2,cc)) . n is Function by PARTFUN1:46; ::_thesis: verum
end;
then reconsider f = Opers (U2,cc) as Function-yielding Function by FUNCOP_1:def_6;
cc is opers_closed by A1, UNIALG_2:def_7;
then A20: cc is_closed_on op by UNIALG_2:def_4;
a in dom the charact of U2 by A12, A14;
then A21: o in dom (Opers (U2,cc)) by UNIALG_2:def_6;
reconsider a = a as OperSymbol of (MSSign U1) ;
MSAlg U1 = MSAlgebra(# (MSSorts U1),(MSCharact U1) #) by MSUALG_1:def_11;
then (Den (a,(MSAlg U1))) . x = ((MSCharact U1) . o) . x by MSUALG_1:def_6
.= ( the charact of U1 . o) . x by MSUALG_1:def_10
.= (f . o) . x by A1, UNIALG_2:def_7
.= (op /. cc) . x by A21, UNIALG_2:def_6
.= (op | ((arity op) -tuples_on cc)) . x by A20, UNIALG_2:def_5
.= ( the charact of U2 . o) . x by A19, FUNCT_1:49
.= ( the Charact of (MSAlg U2) . o) . x by A8, MSUALG_1:def_10
.= (Den (o,(MSAlg U2))) . x by MSUALG_1:def_6 ;
hence (Den (o,(MSAlg U2))) . x = (Den (a,(MSAlg U1))) . x ; ::_thesis: verum
end;
hence for a being OperSymbol of (MSSign U1) st a = o holds
Den (a,(MSAlg U1)) = (Den (o,(MSAlg U2))) | (Args (a,(MSAlg U1))) by A6, FUNCT_1:46; ::_thesis: verum
end;
theorem Th9: :: MSSUBLAT:9
for U1, U2 being Universal_Algebra st U1 is SubAlgebra of U2 holds
the Sorts of (MSAlg U1) is MSSubset of (MSAlg U2)
proof
let U1, U2 be Universal_Algebra; ::_thesis: ( U1 is SubAlgebra of U2 implies the Sorts of (MSAlg U1) is MSSubset of (MSAlg U2) )
set gg1 = (*--> 0) * (signature U2);
set gg2 = (dom (signature U2)) --> z;
reconsider gg1 = (*--> 0) * (signature U2) as Function of (dom (signature U2)),({0} *) by MSUALG_1:2;
A1: MSSign U2 = ManySortedSign(# {0},(dom (signature U2)),gg1,((dom (signature U2)) --> z) #) by MSUALG_1:10;
MSAlg U2 = MSAlgebra(# (MSSorts U2),(MSCharact U2) #) by MSUALG_1:def_11;
then A2: the Sorts of (MSAlg U2) = 0 .--> the carrier of U2 by MSUALG_1:def_9;
assume A3: U1 is SubAlgebra of U2 ; ::_thesis: the Sorts of (MSAlg U1) is MSSubset of (MSAlg U2)
then MSSign U1 = MSSign U2 by Th7;
then reconsider A = MSAlg U1 as non-empty MSAlgebra over MSSign U2 ;
MSAlg U1 = MSAlgebra(# (MSSorts U1),(MSCharact U1) #) by MSUALG_1:def_11;
then A4: the Sorts of A = 0 .--> the carrier of U1 by MSUALG_1:def_9;
A5: 0 in {0} by TARSKI:def_1;
A6: the carrier of U1 is Subset of U2 by A3, UNIALG_2:def_7;
the Sorts of A c= the Sorts of (MSAlg U2)
proof
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in the carrier of (MSSign U2) or the Sorts of A . i c= the Sorts of (MSAlg U2) . i )
assume i in the carrier of (MSSign U2) ; ::_thesis: the Sorts of A . i c= the Sorts of (MSAlg U2) . i
then A7: i = 0 by A1, TARSKI:def_1;
( the Sorts of A . 0 = the carrier of U1 & the Sorts of (MSAlg U2) . 0 = the carrier of U2 ) by A4, A2, A5, FUNCOP_1:7;
hence the Sorts of A . i c= the Sorts of (MSAlg U2) . i by A6, A7; ::_thesis: verum
end;
hence the Sorts of (MSAlg U1) is MSSubset of (MSAlg U2) by PBOOLE:def_18; ::_thesis: verum
end;
theorem Th10: :: MSSUBLAT:10
for U1, U2 being Universal_Algebra st U1 is SubAlgebra of U2 holds
for B being MSSubset of (MSAlg U2) st B = the Sorts of (MSAlg U1) holds
B is opers_closed
proof
let U1, U2 be Universal_Algebra; ::_thesis: ( U1 is SubAlgebra of U2 implies for B being MSSubset of (MSAlg U2) st B = the Sorts of (MSAlg U1) holds
B is opers_closed )
assume A1: U1 is SubAlgebra of U2 ; ::_thesis: for B being MSSubset of (MSAlg U2) st B = the Sorts of (MSAlg U1) holds
B is opers_closed
let B be MSSubset of (MSAlg U2); ::_thesis: ( B = the Sorts of (MSAlg U1) implies B is opers_closed )
assume A2: B = the Sorts of (MSAlg U1) ; ::_thesis: B is opers_closed
let o be OperSymbol of (MSSign U2); :: according to MSUALG_2:def_6 ::_thesis: B is_closed_on o
reconsider a = o as Element of the carrier' of (MSSign U1) by A1, Th7;
set S = (B * the ResultSort of (MSSign U2)) . a;
(B * the ResultSort of (MSSign U2)) . a = ( the Sorts of (MSAlg U1) * the ResultSort of (MSSign U1)) . a by A1, A2, Th7;
then A3: (B * the ResultSort of (MSSign U2)) . a = Result (a,(MSAlg U1)) by MSUALG_1:def_5;
set Z = rng ((Den (o,(MSAlg U2))) | (((B #) * the Arity of (MSSign U2)) . a));
MSSign U1 = MSSign U2 by A1, Th7;
then ( rng (Den (a,(MSAlg U1))) c= Result (a,(MSAlg U1)) & rng ((Den (o,(MSAlg U2))) | (((B #) * the Arity of (MSSign U2)) . a)) = rng ((Den (o,(MSAlg U2))) | (Args (a,(MSAlg U1)))) ) by A2, MSUALG_1:def_4, RELAT_1:def_19;
then rng ((Den (o,(MSAlg U2))) | (((B #) * the Arity of (MSSign U2)) . a)) c= Result (a,(MSAlg U1)) by A1, A2, Th8;
hence B is_closed_on o by A3, MSUALG_2:def_5; ::_thesis: verum
end;
theorem Th11: :: MSSUBLAT:11
for U1, U2 being Universal_Algebra st U1 is SubAlgebra of U2 holds
for B being MSSubset of (MSAlg U2) st B = the Sorts of (MSAlg U1) holds
the Charact of (MSAlg U1) = Opers ((MSAlg U2),B)
proof
let U1, U2 be Universal_Algebra; ::_thesis: ( U1 is SubAlgebra of U2 implies for B being MSSubset of (MSAlg U2) st B = the Sorts of (MSAlg U1) holds
the Charact of (MSAlg U1) = Opers ((MSAlg U2),B) )
assume A1: U1 is SubAlgebra of U2 ; ::_thesis: for B being MSSubset of (MSAlg U2) st B = the Sorts of (MSAlg U1) holds
the Charact of (MSAlg U1) = Opers ((MSAlg U2),B)
let B be MSSubset of (MSAlg U2); ::_thesis: ( B = the Sorts of (MSAlg U1) implies the Charact of (MSAlg U1) = Opers ((MSAlg U2),B) )
set f1 = the Charact of (MSAlg U1);
set f2 = Opers ((MSAlg U2),B);
the carrier' of (MSSign U1) = the carrier' of (MSSign U2)
proof
set ff1 = (*--> 0) * (signature U1);
set ff2 = (dom (signature U1)) --> z;
set gg1 = (*--> 0) * (signature U2);
set gg2 = (dom (signature U2)) --> z;
reconsider ff1 = (*--> 0) * (signature U1) as Function of (dom (signature U1)),({0} *) by MSUALG_1:2;
reconsider gg1 = (*--> 0) * (signature U2) as Function of (dom (signature U2)),({0} *) by MSUALG_1:2;
A2: MSSign U2 = ManySortedSign(# {0},(dom (signature U2)),gg1,((dom (signature U2)) --> z) #) by MSUALG_1:10;
( U1,U2 are_similar & MSSign U1 = ManySortedSign(# {0},(dom (signature U1)),ff1,((dom (signature U1)) --> z) #) ) by A1, MSUALG_1:10, UNIALG_2:13;
hence the carrier' of (MSSign U1) = the carrier' of (MSSign U2) by A2, UNIALG_2:def_1; ::_thesis: verum
end;
then reconsider f1 = the Charact of (MSAlg U1) as ManySortedSet of the carrier' of (MSSign U2) ;
assume A3: B = the Sorts of (MSAlg U1) ; ::_thesis: the Charact of (MSAlg U1) = Opers ((MSAlg U2),B)
for x being set st x in the carrier' of (MSSign U2) holds
f1 . x = (Opers ((MSAlg U2),B)) . x
proof
let x be set ; ::_thesis: ( x in the carrier' of (MSSign U2) implies f1 . x = (Opers ((MSAlg U2),B)) . x )
assume A4: x in the carrier' of (MSSign U2) ; ::_thesis: f1 . x = (Opers ((MSAlg U2),B)) . x
then reconsider y = x as OperSymbol of (MSSign U2) ;
reconsider x = x as OperSymbol of (MSSign U1) by A1, A4, Th7;
B is opers_closed by A1, A3, Th10;
then ( (Opers ((MSAlg U2),B)) . y = y /. B & B is_closed_on y ) by MSUALG_2:def_6, MSUALG_2:def_8;
then A5: (Opers ((MSAlg U2),B)) . y = (Den (y,(MSAlg U2))) | (((B #) * the Arity of (MSSign U2)) . y) by MSUALG_2:def_7;
((B #) * the Arity of (MSSign U1)) . x = (( the Sorts of (MSAlg U1) #) * the Arity of (MSSign U1)) . x by A1, A3, Th7;
then (Opers ((MSAlg U2),B)) . y = (Den (y,(MSAlg U2))) | ((( the Sorts of (MSAlg U1) #) * the Arity of (MSSign U1)) . x) by A1, A5, Th7;
then ( f1 . x = Den (x,(MSAlg U1)) & (Opers ((MSAlg U2),B)) . y = (Den (y,(MSAlg U2))) | (Args (x,(MSAlg U1))) ) by MSUALG_1:def_4, MSUALG_1:def_6;
hence f1 . x = (Opers ((MSAlg U2),B)) . x by A1, A3, Th8; ::_thesis: verum
end;
hence the Charact of (MSAlg U1) = Opers ((MSAlg U2),B) by PBOOLE:3; ::_thesis: verum
end;
theorem Th12: :: MSSUBLAT:12
for U1, U2 being Universal_Algebra st U1 is SubAlgebra of U2 holds
MSAlg U1 is MSSubAlgebra of MSAlg U2
proof
let U1, U2 be Universal_Algebra; ::_thesis: ( U1 is SubAlgebra of U2 implies MSAlg U1 is MSSubAlgebra of MSAlg U2 )
assume A1: U1 is SubAlgebra of U2 ; ::_thesis: MSAlg U1 is MSSubAlgebra of MSAlg U2
then MSSign U1 = MSSign U2 by Th7;
then reconsider A = MSAlg U1 as non-empty MSAlgebra over MSSign U2 ;
A is MSSubAlgebra of MSAlg U2
proof
thus the Sorts of A is MSSubset of (MSAlg U2) by A1, Th9; :: according to MSUALG_2:def_9 ::_thesis: for b1 being ManySortedSubset of the Sorts of (MSAlg U2) holds
( not b1 = the Sorts of A or ( b1 is opers_closed & the Charact of A = Opers ((MSAlg U2),b1) ) )
let B be MSSubset of (MSAlg U2); ::_thesis: ( not B = the Sorts of A or ( B is opers_closed & the Charact of A = Opers ((MSAlg U2),B) ) )
assume A2: B = the Sorts of A ; ::_thesis: ( B is opers_closed & the Charact of A = Opers ((MSAlg U2),B) )
hence B is opers_closed by A1, Th10; ::_thesis: the Charact of A = Opers ((MSAlg U2),B)
thus the Charact of A = Opers ((MSAlg U2),B) by A1, A2, Th11; ::_thesis: verum
end;
hence MSAlg U1 is MSSubAlgebra of MSAlg U2 ; ::_thesis: verum
end;
theorem Th13: :: MSSUBLAT:13
for U1, U2 being Universal_Algebra st MSAlg U1 is MSSubAlgebra of MSAlg U2 holds
the carrier of U1 is Subset of U2
proof
let U1, U2 be Universal_Algebra; ::_thesis: ( MSAlg U1 is MSSubAlgebra of MSAlg U2 implies the carrier of U1 is Subset of U2 )
set MU1 = MSAlg U1;
set MU2 = MSAlg U2;
assume A1: MSAlg U1 is MSSubAlgebra of MSAlg U2 ; ::_thesis: the carrier of U1 is Subset of U2
then reconsider MU1 = MSAlg U1 as MSAlgebra over MSSign U2 ;
reconsider C = the Sorts of MU1 as MSSubset of (MSAlg U2) by A1, MSUALG_2:def_9;
set gg1 = (*--> 0) * (signature U2);
set gg2 = (dom (signature U2)) --> z;
reconsider gg1 = (*--> 0) * (signature U2) as Function of (dom (signature U2)),({0} *) by MSUALG_1:2;
reconsider C1 = C as ManySortedSet of the carrier of (MSSign U2) ;
A2: 0 in {0} by TARSKI:def_1;
MSAlg U2 = MSAlgebra(# (MSSorts U2),(MSCharact U2) #) by MSUALG_1:def_11;
then A3: C1 c= MSSorts U2 by PBOOLE:def_18;
( MSSign U2 = ManySortedSign(# {0},(dom (signature U2)),gg1,((dom (signature U2)) --> z) #) & MSSorts U2 = 0 .--> the carrier of U2 ) by MSUALG_1:10, MSUALG_1:def_9;
then ( MU1 = MSAlgebra(# (MSSorts U1),(MSCharact U1) #) & C1 . 0 c= ({0} --> the carrier of U2) . 0 ) by A3, MSUALG_1:def_11, PBOOLE:def_2;
then (MSSorts U1) . 0 c= the carrier of U2 by A2, FUNCOP_1:7;
then (0 .--> the carrier of U1) . 0 c= the carrier of U2 by MSUALG_1:def_9;
hence the carrier of U1 is Subset of U2 by A2, FUNCOP_1:7; ::_thesis: verum
end;
theorem Th14: :: MSSUBLAT:14
for U1, U2 being Universal_Algebra st MSAlg U1 is MSSubAlgebra of MSAlg U2 holds
for B being non empty Subset of U2 st B = the carrier of U1 holds
B is opers_closed
proof
let U1, U2 be Universal_Algebra; ::_thesis: ( MSAlg U1 is MSSubAlgebra of MSAlg U2 implies for B being non empty Subset of U2 st B = the carrier of U1 holds
B is opers_closed )
set MU1 = MSAlg U1;
set MU2 = MSAlg U2;
A1: MSAlg U2 = MSAlgebra(# (MSSorts U2),(MSCharact U2) #) by MSUALG_1:def_11;
assume A2: MSAlg U1 is MSSubAlgebra of MSAlg U2 ; ::_thesis: for B being non empty Subset of U2 st B = the carrier of U1 holds
B is opers_closed
then reconsider MU1 = MSAlg U1 as MSAlgebra over MSSign U2 ;
let B be non empty Subset of U2; ::_thesis: ( B = the carrier of U1 implies B is opers_closed )
assume A3: B = the carrier of U1 ; ::_thesis: B is opers_closed
let o be operation of U2; :: according to UNIALG_2:def_4 ::_thesis: B is_closed_on o
reconsider C = the Sorts of MU1 as MSSubset of (MSAlg U2) by A2, MSUALG_2:def_9;
A4: MU1 = MSAlgebra(# (MSSorts U1),(MSCharact U1) #) by MSUALG_1:def_11;
set gg1 = (*--> 0) * (signature U2);
set gg2 = (dom (signature U2)) --> z;
reconsider gg1 = (*--> 0) * (signature U2) as Function of (dom (signature U2)),({0} *) by MSUALG_1:2;
A5: MSSign U2 = ManySortedSign(# {0},(dom (signature U2)),gg1,((dom (signature U2)) --> z) #) by MSUALG_1:10;
A6: C is opers_closed by A2, MSUALG_2:def_9;
thus B is_closed_on o ::_thesis: verum
proof
A7: 0 in {0} by TARSKI:def_1;
let s be FinSequence of B; :: according to UNIALG_2:def_3 ::_thesis: ( not len s = arity o or o . s in B )
consider n being set such that
A8: n in dom the charact of U2 and
A9: o = the charact of U2 . n by FUNCT_1:def_3;
A10: ( dom the charact of U2 = Seg (len the charact of U2) & dom (signature U2) = Seg (len (signature U2)) ) by FINSEQ_1:def_3;
then A11: n in dom (signature U2) by A8, UNIALG_1:def_4;
reconsider n = n as OperSymbol of (MSSign U2) by A5, A8, A10, UNIALG_1:def_4;
assume A12: len s = arity o ; ::_thesis: o . s in B
ex y being set st
( y in dom ((Den (n,(MSAlg U2))) | (((C #) * the Arity of (MSSign U2)) . n)) & ((Den (n,(MSAlg U2))) | (((C #) * the Arity of (MSSign U2)) . n)) . y = o . s )
proof
take s ; ::_thesis: ( s in dom ((Den (n,(MSAlg U2))) | (((C #) * the Arity of (MSSign U2)) . n)) & ((Den (n,(MSAlg U2))) | (((C #) * the Arity of (MSSign U2)) . n)) . s = o . s )
thus s in dom ((Den (n,(MSAlg U2))) | (((C #) * the Arity of (MSSign U2)) . n)) ::_thesis: ((Den (n,(MSAlg U2))) | (((C #) * the Arity of (MSSign U2)) . n)) . s = o . s
proof
(arity o) |-> 0 is FinSequence of the carrier of (MSSign U2) by A5, FINSEQ_2:63;
then reconsider ao0 = (arity o) |-> 0 as Element of the carrier of (MSSign U2) * by FINSEQ_1:def_11;
A13: now__::_thesis:_(_Seg_(arity_o)_=_{}_implies_(arity_o)_|->_0_is_FinSequence_of_the_carrier_of_(MSSign_U2)_)
assume Seg (arity o) = {} ; ::_thesis: (arity o) |-> 0 is FinSequence of the carrier of (MSSign U2)
then (arity o) |-> 0 = <*> the carrier of (MSSign U2) ;
hence (arity o) |-> 0 is FinSequence of the carrier of (MSSign U2) ; ::_thesis: verum
end;
( Seg (arity o) <> {} implies ( dom ((arity o) |-> 0) = Seg (arity o) & rng ((arity o) |-> 0) c= the carrier of (MSSign U2) ) ) by A5, FUNCOP_1:13;
then (arity o) |-> 0 is FinSequence of the carrier of (MSSign U2) by A13, FINSEQ_1:def_4;
then reconsider aro = (arity o) |-> 0 as Element of the carrier of (MSSign U2) * by FINSEQ_1:def_11;
A14: dom the Arity of (MSSign U2) = the carrier' of (MSSign U2) by FUNCT_2:def_1;
the Sorts of (MSAlg U2) = 0 .--> the carrier of U2 by A1, MSUALG_1:def_9;
then A15: the Sorts of (MSAlg U2) * aro = (arity o) |-> the carrier of U2 by FINSEQ_2:144
.= (Seg (arity o)) --> the carrier of U2 ;
dom s = Seg (arity o) by A12, FINSEQ_1:def_3;
then A16: dom s = dom ( the Sorts of (MSAlg U2) * aro) by A15, FUNCT_2:def_1;
A17: for x being set st x in dom ( the Sorts of (MSAlg U2) * aro) holds
s . x in ( the Sorts of (MSAlg U2) * aro) . x
proof
let x be set ; ::_thesis: ( x in dom ( the Sorts of (MSAlg U2) * aro) implies s . x in ( the Sorts of (MSAlg U2) * aro) . x )
rng s c= B by FINSEQ_1:def_4;
then A18: rng s c= the carrier of U2 by XBOOLE_1:1;
assume A19: x in dom ( the Sorts of (MSAlg U2) * aro) ; ::_thesis: s . x in ( the Sorts of (MSAlg U2) * aro) . x
s . x in rng s by A16, A19, FUNCT_1:def_3;
then A20: ( 0 in {0} & s . x in the carrier of U2 ) by A18, TARSKI:def_1;
( the Sorts of (MSAlg U2) * aro) . x = the Sorts of (MSAlg U2) . (aro . x) by A19, FUNCT_1:12
.= (MSSorts U2) . 0 by A1
.= (0 .--> the carrier of U2) . 0 by MSUALG_1:def_9 ;
hence s . x in ( the Sorts of (MSAlg U2) * aro) . x by A20, FUNCOP_1:7; ::_thesis: verum
end;
dom (Den (n,(MSAlg U2))) = Args (n,(MSAlg U2)) by FUNCT_2:def_1;
then dom (Den (n,(MSAlg U2))) = (( the Sorts of (MSAlg U2) #) * the Arity of (MSSign U2)) . n by MSUALG_1:def_4
.= ( the Sorts of (MSAlg U2) #) . (((*--> 0) * (signature U2)) . n) by A5, A14, FUNCT_1:13
.= ( the Sorts of (MSAlg U2) #) . ((*--> 0) . ((signature U2) . n)) by A11, FUNCT_1:13
.= ( the Sorts of (MSAlg U2) #) . ((*--> 0) . (arity o)) by A9, A11, UNIALG_1:def_4
.= ( the Sorts of (MSAlg U2) #) . ((arity o) |-> 0) by FINSEQ_2:def_6 ;
then dom (Den (n,(MSAlg U2))) = product ( the Sorts of (MSAlg U2) * aro) by FINSEQ_2:def_5;
then A21: s in dom (Den (n,(MSAlg U2))) by A16, A17, CARD_3:def_5;
A22: s is Element of (len s) -tuples_on B by FINSEQ_2:92;
A23: 0 in {0} by TARSKI:def_1;
A24: n in dom (signature U2) by A8, A10, UNIALG_1:def_4;
A25: C = 0 .--> the carrier of U1 by A4, MSUALG_1:def_9;
then dom C = {0} by FUNCOP_1:13;
then A26: 0 in dom C by TARSKI:def_1;
( dom (*--> 0) = NAT & (signature U2) . n = arity o ) by A9, A11, FUNCT_2:def_1, UNIALG_1:def_4;
then A27: n in dom ((*--> 0) * (signature U2)) by A24, FUNCT_1:11;
then ((C #) * the Arity of (MSSign U2)) . n = (C #) . (((*--> 0) * (signature U2)) . n) by A5, FUNCT_1:13
.= (C #) . ((*--> 0) . ((signature U2) . n)) by A27, FUNCT_1:12
.= (C #) . ((*--> 0) . (arity o)) by A9, A24, UNIALG_1:def_4
.= (C #) . ((arity o) |-> 0) by FINSEQ_2:def_6 ;
then ((C #) * the Arity of (MSSign U2)) . n = product (C * ao0) by FINSEQ_2:def_5
.= product ((Seg (arity o)) --> (C . 0)) by A26, FUNCOP_1:17
.= product ((Seg (arity o)) --> B) by A3, A25, A23, FUNCOP_1:7
.= Funcs ((Seg (arity o)),B) by CARD_3:11
.= (arity o) -tuples_on B by FINSEQ_2:93 ;
then s in (dom (Den (n,(MSAlg U2)))) /\ (((C #) * the Arity of (MSSign U2)) . n) by A12, A21, A22, XBOOLE_0:def_4;
hence s in dom ((Den (n,(MSAlg U2))) | (((C #) * the Arity of (MSSign U2)) . n)) by RELAT_1:61; ::_thesis: verum
end;
hence ((Den (n,(MSAlg U2))) | (((C #) * the Arity of (MSSign U2)) . n)) . s = (Den (n,(MSAlg U2))) . s by FUNCT_1:47
.= ((MSCharact U2) . n) . s by A1, MSUALG_1:def_6
.= o . s by A9, MSUALG_1:def_10 ;
::_thesis: verum
end;
then A28: o . s in rng ((Den (n,(MSAlg U2))) | (((C #) * the Arity of (MSSign U2)) . n)) by FUNCT_1:def_3;
C is_closed_on n by A6, MSUALG_2:def_6;
then A29: rng ((Den (n,(MSAlg U2))) | (((C #) * the Arity of (MSSign U2)) . n)) c= (C * the ResultSort of (MSSign U2)) . n by MSUALG_2:def_5;
n in dom ((dom (signature U2)) --> 0) by A11, FUNCOP_1:13;
then (C * the ResultSort of (MSSign U2)) . n = C . (((dom (signature U2)) --> 0) . n) by A5, FUNCT_1:13
.= the Sorts of MU1 . 0 by A11, FUNCOP_1:7
.= (0 .--> the carrier of U1) . 0 by A4, MSUALG_1:def_9
.= B by A3, A7, FUNCOP_1:7 ;
hence o . s in B by A29, A28; ::_thesis: verum
end;
end;
theorem Th15: :: MSSUBLAT:15
for U1, U2 being Universal_Algebra st MSAlg U1 is MSSubAlgebra of MSAlg U2 holds
for B being non empty Subset of U2 st B = the carrier of U1 holds
the charact of U1 = Opers (U2,B)
proof
let U1, U2 be Universal_Algebra; ::_thesis: ( MSAlg U1 is MSSubAlgebra of MSAlg U2 implies for B being non empty Subset of U2 st B = the carrier of U1 holds
the charact of U1 = Opers (U2,B) )
set MU1 = MSAlg U1;
set MU2 = MSAlg U2;
A1: MSAlg U2 = MSAlgebra(# (MSSorts U2),(MSCharact U2) #) by MSUALG_1:def_11;
assume A2: MSAlg U1 is MSSubAlgebra of MSAlg U2 ; ::_thesis: for B being non empty Subset of U2 st B = the carrier of U1 holds
the charact of U1 = Opers (U2,B)
then reconsider MU1 = MSAlg U1 as MSAlgebra over MSSign U2 ;
reconsider C = the Sorts of MU1 as MSSubset of (MSAlg U2) by A2, MSUALG_2:def_9;
A3: the Charact of MU1 = Opers ((MSAlg U2),C) by A2, MSUALG_2:def_9;
set gg1 = (*--> 0) * (signature U2);
set gg2 = (dom (signature U2)) --> z;
reconsider gg1 = (*--> 0) * (signature U2) as Function of (dom (signature U2)),({0} *) by MSUALG_1:2;
A4: MSSign U2 = ManySortedSign(# {0},(dom (signature U2)),gg1,((dom (signature U2)) --> z) #) by MSUALG_1:10;
let B be non empty Subset of U2; ::_thesis: ( B = the carrier of U1 implies the charact of U1 = Opers (U2,B) )
assume A5: B = the carrier of U1 ; ::_thesis: the charact of U1 = Opers (U2,B)
then reconsider ch1 = the charact of U1 as PFuncFinSequence of B ;
A6: MU1 = MSAlgebra(# (MSSorts U1),(MSCharact U1) #) by MSUALG_1:def_11;
then A7: dom ch1 = dom the Charact of MU1 by MSUALG_1:def_10
.= the carrier' of (MSSign U2) by PARTFUN1:def_2
.= Seg (len (signature U2)) by A4, FINSEQ_1:def_3
.= Seg (len the charact of U2) by UNIALG_1:def_4
.= dom the charact of U2 by FINSEQ_1:def_3 ;
A8: C is opers_closed by A2, MSUALG_2:def_9;
for n being set
for o being operation of U2 st n in dom ch1 & o = the charact of U2 . n holds
ch1 . n = o /. B
proof
A9: C = 0 .--> the carrier of U1 by A6, MSUALG_1:def_9;
then dom C = {0} by FUNCOP_1:13;
then A10: 0 in dom C by TARSKI:def_1;
let n be set ; ::_thesis: for o being operation of U2 st n in dom ch1 & o = the charact of U2 . n holds
ch1 . n = o /. B
let o be operation of U2; ::_thesis: ( n in dom ch1 & o = the charact of U2 . n implies ch1 . n = o /. B )
assume that
A11: n in dom ch1 and
A12: o = the charact of U2 . n ; ::_thesis: ch1 . n = o /. B
n in dom the Charact of (MSAlg U2) by A1, A7, A11, MSUALG_1:def_10;
then reconsider N = n as OperSymbol of (MSSign U2) by PARTFUN1:def_2;
A13: ( dom the charact of U2 = Seg (len the charact of U2) & dom (signature U2) = Seg (len (signature U2)) ) by FINSEQ_1:def_3;
then A14: N in dom (signature U2) by A7, A11, UNIALG_1:def_4;
(arity o) |-> 0 is FinSequence of the carrier of (MSSign U2) by A4, FINSEQ_2:63;
then reconsider ao0 = (arity o) |-> 0 as Element of the carrier of (MSSign U2) * by FINSEQ_1:def_11;
A15: C is_closed_on N by A8, MSUALG_2:def_6;
B is opers_closed by A2, A5, Th14;
then A16: B is_closed_on o by UNIALG_2:def_4;
A17: 0 in {0} by TARSKI:def_1;
N in dom (signature U2) by A7, A11, A13, UNIALG_1:def_4;
then ( dom (*--> 0) = NAT & (signature U2) . N = arity o ) by A12, FUNCT_2:def_1, UNIALG_1:def_4;
then A18: N in dom ((*--> 0) * (signature U2)) by A14, FUNCT_1:11;
then ((C #) * the Arity of (MSSign U2)) . N = (C #) . (((*--> 0) * (signature U2)) . N) by A4, FUNCT_1:13
.= (C #) . ((*--> 0) . ((signature U2) . N)) by A18, FUNCT_1:12
.= (C #) . ((*--> 0) . (arity o)) by A12, A14, UNIALG_1:def_4
.= (C #) . ((arity o) |-> 0) by FINSEQ_2:def_6 ;
then A19: ((C #) * the Arity of (MSSign U2)) . N = product (C * ao0) by FINSEQ_2:def_5
.= product ((Seg (arity o)) --> (C . 0)) by A10, FUNCOP_1:17
.= product ((Seg (arity o)) --> B) by A5, A9, A17, FUNCOP_1:7
.= Funcs ((Seg (arity o)),B) by CARD_3:11
.= (arity o) -tuples_on B by FINSEQ_2:93 ;
ch1 . N = the Charact of MU1 . N by A6, MSUALG_1:def_10
.= N /. C by A3, MSUALG_2:def_8
.= (Den (N,(MSAlg U2))) | (((C #) * the Arity of (MSSign U2)) . N) by A15, MSUALG_2:def_7
.= ((MSCharact U2) . N) | (((C #) * the Arity of (MSSign U2)) . N) by A1, MSUALG_1:def_6
.= o | ((arity o) -tuples_on B) by A12, A19, MSUALG_1:def_10 ;
hence ch1 . n = o /. B by A16, UNIALG_2:def_5; ::_thesis: verum
end;
hence the charact of U1 = Opers (U2,B) by A7, UNIALG_2:def_6; ::_thesis: verum
end;
theorem Th16: :: MSSUBLAT:16
for U1, U2 being Universal_Algebra st MSAlg U1 is MSSubAlgebra of MSAlg U2 holds
U1 is SubAlgebra of U2
proof
let U1, U2 be Universal_Algebra; ::_thesis: ( MSAlg U1 is MSSubAlgebra of MSAlg U2 implies U1 is SubAlgebra of U2 )
assume A1: MSAlg U1 is MSSubAlgebra of MSAlg U2 ; ::_thesis: U1 is SubAlgebra of U2
hence the carrier of U1 is Subset of U2 by Th13; :: according to UNIALG_2:def_7 ::_thesis: for b1 being Element of K19( the carrier of U2) holds
( not b1 = the carrier of U1 or ( the charact of U1 = Opers (U2,b1) & b1 is opers_closed ) )
let B be non empty Subset of U2; ::_thesis: ( not B = the carrier of U1 or ( the charact of U1 = Opers (U2,B) & B is opers_closed ) )
assume B = the carrier of U1 ; ::_thesis: ( the charact of U1 = Opers (U2,B) & B is opers_closed )
hence ( the charact of U1 = Opers (U2,B) & B is opers_closed ) by A1, Th14, Th15; ::_thesis: verum
end;
theorem Th17: :: MSSUBLAT:17
for MS being non void 1 -element segmental ManySortedSign
for A being non-empty MSAlgebra over MS
for B being non-empty MSSubAlgebra of A holds the carrier of (1-Alg B) is Subset of (1-Alg A)
proof
let MS be non void 1 -element segmental ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over MS
for B being non-empty MSSubAlgebra of A holds the carrier of (1-Alg B) is Subset of (1-Alg A)
let A be non-empty MSAlgebra over MS; ::_thesis: for B being non-empty MSSubAlgebra of A holds the carrier of (1-Alg B) is Subset of (1-Alg A)
let B be non-empty MSSubAlgebra of A; ::_thesis: the carrier of (1-Alg B) is Subset of (1-Alg A)
the Sorts of B is MSSubset of A by MSUALG_2:def_9;
then A1: the Sorts of B c= the Sorts of A by PBOOLE:def_18;
1-Alg B = UAStr(# (the_sort_of B),(the_charact_of B) #) by MSUALG_1:def_14;
then reconsider c = the carrier of (1-Alg B) as Component of the Sorts of B by MSUALG_1:def_12;
1-Alg A = UAStr(# (the_sort_of A),(the_charact_of A) #) by MSUALG_1:def_14;
then reconsider d = the carrier of (1-Alg A) as Component of the Sorts of A by MSUALG_1:def_12;
A2: dom the Sorts of A = the carrier of MS by PARTFUN1:def_2;
then consider dr being set such that
A3: dr in the carrier of MS and
A4: d = the Sorts of A . dr by FUNCT_1:def_3;
dom the Sorts of A = dom the Sorts of B by A2, PARTFUN1:def_2;
then consider cr being set such that
A5: cr in the carrier of MS and
A6: c = the Sorts of B . cr by A2, FUNCT_1:def_3;
cr = dr by A5, A3, STRUCT_0:def_10;
hence the carrier of (1-Alg B) is Subset of (1-Alg A) by A1, A5, A6, A4, PBOOLE:def_2; ::_thesis: verum
end;
theorem Th18: :: MSSUBLAT:18
for MS being non void 1 -element segmental ManySortedSign
for A being non-empty MSAlgebra over MS
for B being non-empty MSSubAlgebra of A
for S being non empty Subset of (1-Alg A) st S = the carrier of (1-Alg B) holds
S is opers_closed
proof
let MS be non void 1 -element segmental ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over MS
for B being non-empty MSSubAlgebra of A
for S being non empty Subset of (1-Alg A) st S = the carrier of (1-Alg B) holds
S is opers_closed
let A be non-empty MSAlgebra over MS; ::_thesis: for B being non-empty MSSubAlgebra of A
for S being non empty Subset of (1-Alg A) st S = the carrier of (1-Alg B) holds
S is opers_closed
let B be non-empty MSSubAlgebra of A; ::_thesis: for S being non empty Subset of (1-Alg A) st S = the carrier of (1-Alg B) holds
S is opers_closed
reconsider C = the Sorts of B as MSSubset of A by MSUALG_2:def_9;
A1: C is opers_closed by MSUALG_2:def_9;
A2: 1-Alg B = UAStr(# (the_sort_of B),(the_charact_of B) #) by MSUALG_1:def_14;
let S be non empty Subset of (1-Alg A); ::_thesis: ( S = the carrier of (1-Alg B) implies S is opers_closed )
assume A3: S = the carrier of (1-Alg B) ; ::_thesis: S is opers_closed
set 1A = 1-Alg A;
A4: 1-Alg A = UAStr(# (the_sort_of A),(the_charact_of A) #) by MSUALG_1:def_14;
let o be operation of (1-Alg A); :: according to UNIALG_2:def_4 ::_thesis: S is_closed_on o
A5: dom the Sorts of A = the carrier of MS by PARTFUN1:def_2;
then A6: dom the Sorts of A = dom the Sorts of B by PARTFUN1:def_2;
thus S is_closed_on o ::_thesis: verum
proof
reconsider com = S as Component of the Sorts of B by A2, A3, MSUALG_1:def_12;
consider n being set such that
A7: n in dom the charact of (1-Alg A) and
A8: o = the charact of (1-Alg A) . n by FUNCT_1:def_3;
n in dom the Charact of A by A4, A7, MSUALG_1:def_13;
then reconsider n = n as OperSymbol of MS by PARTFUN1:def_2;
reconsider crn = C . ( the ResultSort of MS . n) as Component of the Sorts of B by A5, A6, FUNCT_1:def_3;
let s be FinSequence of S; :: according to UNIALG_2:def_3 ::_thesis: ( not len s = arity o or o . s in S )
A9: dom the Arity of MS = the carrier' of MS by FUNCT_2:def_1;
assume A10: len s = arity o ; ::_thesis: o . s in S
ex y being set st
( y in dom ((Den (n,A)) | (((C #) * the Arity of MS) . n)) & ((Den (n,A)) | (((C #) * the Arity of MS) . n)) . y = o . s )
proof
take s ; ::_thesis: ( s in dom ((Den (n,A)) | (((C #) * the Arity of MS) . n)) & ((Den (n,A)) | (((C #) * the Arity of MS) . n)) . s = o . s )
A11: the Charact of A . n = the charact of (1-Alg A) . n by A4, MSUALG_1:def_13;
thus s in dom ((Den (n,A)) | (((C #) * the Arity of MS) . n)) ::_thesis: ((Den (n,A)) | (((C #) * the Arity of MS) . n)) . s = o . s
proof
rng s c= S by FINSEQ_1:def_4;
then rng s c= the carrier of (1-Alg A) by XBOOLE_1:1;
then reconsider s1 = s as FinSequence of the carrier of (1-Alg A) by FINSEQ_1:def_4;
reconsider An = the Arity of MS . n as Element of the carrier of MS * ;
set f = the Sorts of A * An;
consider d being set such that
A12: d in dom o by XBOOLE_0:def_1;
o in PFuncs (( the carrier of (1-Alg A) *), the carrier of (1-Alg A)) by PARTFUN1:45;
then ex o1 being Function st
( o1 = o & dom o1 c= the carrier of (1-Alg A) * & rng o1 c= the carrier of (1-Alg A) ) by PARTFUN1:def_3;
then reconsider d = d as FinSequence of the carrier of (1-Alg A) by A12, FINSEQ_1:def_11;
A13: dom (Den (n,A)) = Args (n,A) by FUNCT_2:def_1
.= (len (the_arity_of n)) -tuples_on the carrier of (1-Alg A) by A4, MSUALG_1:6 ;
dom (Den (n,A)) = Args (n,A) by FUNCT_2:def_1;
then dom (Den (n,A)) = (( the Sorts of A #) * the Arity of MS) . n by MSUALG_1:def_4
.= ( the Sorts of A #) . ( the Arity of MS . n) by A9, FUNCT_1:13 ;
then A14: dom (Den (n,A)) = product ( the Sorts of A * An) by FINSEQ_2:def_5;
A15: o = the Charact of A . n by A4, A8, MSUALG_1:def_13
.= Den (n,A) by MSUALG_1:def_6 ;
len d = len s1 by A10, A12, MARGREL1:def_25;
then len s = len (the_arity_of n) by A12, A15, A13, CARD_1:def_7;
then A16: dom s = Seg (len (the_arity_of n)) by FINSEQ_1:def_3
.= dom (the_arity_of n) by FINSEQ_1:def_3
.= dom An by MSUALG_1:def_1 ;
A17: dom s c= dom (C * An)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom s or x in dom (C * An) )
assume A18: x in dom s ; ::_thesis: x in dom (C * An)
then ( rng An c= the carrier of MS & An . x in rng An ) by A16, FINSEQ_1:def_4, FUNCT_1:def_3;
then An . x in the carrier of MS ;
then An . x in dom C by PARTFUN1:def_2;
hence x in dom (C * An) by A16, A18, FUNCT_1:11; ::_thesis: verum
end;
dom (C * An) c= dom s by A16, RELAT_1:25;
then A19: dom s = dom (C * An) by A17, XBOOLE_0:def_10;
A20: for x being set st x in dom s holds
s . x in (C * An) . x
proof
let x be set ; ::_thesis: ( x in dom s implies s . x in (C * An) . x )
A21: rng s c= S by FINSEQ_1:def_4;
assume A22: x in dom s ; ::_thesis: s . x in (C * An) . x
then A23: s . x in rng s by FUNCT_1:def_3;
dom s c= dom An by A19, RELAT_1:25;
then ( rng An c= the carrier of MS & An . x in rng An ) by A22, FINSEQ_1:def_4, FUNCT_1:def_3;
then An . x in the carrier of MS ;
then A24: An . x in dom C by PARTFUN1:def_2;
(C * An) . x = C . (An . x) by A17, A22, FUNCT_1:12;
then reconsider canx = (C * An) . x as Component of C by A24, FUNCT_1:def_3;
(C * An) . x = canx
.= S by A2, A3, MSUALG_1:def_12 ;
hence s . x in (C * An) . x by A23, A21; ::_thesis: verum
end;
A25: dom ( the Sorts of A * An) c= dom s
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom ( the Sorts of A * An) or x in dom s )
assume x in dom ( the Sorts of A * An) ; ::_thesis: x in dom s
hence x in dom s by A16, FUNCT_1:11; ::_thesis: verum
end;
A26: for x being set st x in dom ( the Sorts of A * An) holds
s . x in ( the Sorts of A * An) . x
proof
let x be set ; ::_thesis: ( x in dom ( the Sorts of A * An) implies s . x in ( the Sorts of A * An) . x )
A27: rng s c= S by FINSEQ_1:def_4;
assume A28: x in dom ( the Sorts of A * An) ; ::_thesis: s . x in ( the Sorts of A * An) . x
then ( the Sorts of A * An) . x in rng ( the Sorts of A * An) by FUNCT_1:def_3;
then reconsider fx = ( the Sorts of A * An) . x as Component of the Sorts of A by FUNCT_1:14;
s . x in rng s by A25, A28, FUNCT_1:def_3;
then ( fx = the_sort_of A & s . x in S ) by A27, MSUALG_1:def_12;
hence s . x in ( the Sorts of A * An) . x by A4; ::_thesis: verum
end;
dom the Arity of MS = the carrier' of MS by FUNCT_2:def_1;
then ((C #) * the Arity of MS) . n = (C #) . An by FUNCT_1:13
.= product (C * An) by FINSEQ_2:def_5 ;
then A29: s in ((C #) * the Arity of MS) . n by A19, A20, CARD_3:9;
dom s c= dom ( the Sorts of A * An)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom s or x in dom ( the Sorts of A * An) )
assume A30: x in dom s ; ::_thesis: x in dom ( the Sorts of A * An)
then ( rng An c= the carrier of MS & An . x in rng An ) by A16, FINSEQ_1:def_4, FUNCT_1:def_3;
then An . x in the carrier of MS ;
then An . x in dom the Sorts of A by PARTFUN1:def_2;
hence x in dom ( the Sorts of A * An) by A16, A30, FUNCT_1:11; ::_thesis: verum
end;
then dom s = dom ( the Sorts of A * An) by A25, XBOOLE_0:def_10;
then s in dom (Den (n,A)) by A14, A26, CARD_3:9;
then s in (dom (Den (n,A))) /\ (((C #) * the Arity of MS) . n) by A29, XBOOLE_0:def_4;
hence s in dom ((Den (n,A)) | (((C #) * the Arity of MS) . n)) by RELAT_1:61; ::_thesis: verum
end;
hence ((Den (n,A)) | (((C #) * the Arity of MS) . n)) . s = (Den (n,A)) . s by FUNCT_1:47
.= o . s by A8, A11, MSUALG_1:def_6 ;
::_thesis: verum
end;
then A31: o . s in rng ((Den (n,A)) | (((C #) * the Arity of MS) . n)) by FUNCT_1:def_3;
dom the ResultSort of MS = the carrier' of MS by FUNCT_2:def_1;
then A32: (C * the ResultSort of MS) . n = crn by FUNCT_1:13
.= com by MSUALG_1:5 ;
C is_closed_on n by A1, MSUALG_2:def_6;
then rng ((Den (n,A)) | (((C #) * the Arity of MS) . n)) c= (C * the ResultSort of MS) . n by MSUALG_2:def_5;
hence o . s in S by A31, A32; ::_thesis: verum
end;
end;
theorem Th19: :: MSSUBLAT:19
for MS being non void 1 -element segmental ManySortedSign
for A being non-empty MSAlgebra over MS
for B being non-empty MSSubAlgebra of A
for S being non empty Subset of (1-Alg A) st S = the carrier of (1-Alg B) holds
the charact of (1-Alg B) = Opers ((1-Alg A),S)
proof
let MS be non void 1 -element segmental ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over MS
for B being non-empty MSSubAlgebra of A
for S being non empty Subset of (1-Alg A) st S = the carrier of (1-Alg B) holds
the charact of (1-Alg B) = Opers ((1-Alg A),S)
let A be non-empty MSAlgebra over MS; ::_thesis: for B being non-empty MSSubAlgebra of A
for S being non empty Subset of (1-Alg A) st S = the carrier of (1-Alg B) holds
the charact of (1-Alg B) = Opers ((1-Alg A),S)
let B be non-empty MSSubAlgebra of A; ::_thesis: for S being non empty Subset of (1-Alg A) st S = the carrier of (1-Alg B) holds
the charact of (1-Alg B) = Opers ((1-Alg A),S)
reconsider C = the Sorts of B as MSSubset of A by MSUALG_2:def_9;
A1: the Charact of B = Opers (A,C) by MSUALG_2:def_9;
set 1B = 1-Alg B;
set 1A = 1-Alg A;
A2: 1-Alg A = UAStr(# (the_sort_of A),(the_charact_of A) #) by MSUALG_1:def_14;
set f1 = the charact of (1-Alg B);
let S be non empty Subset of (1-Alg A); ::_thesis: ( S = the carrier of (1-Alg B) implies the charact of (1-Alg B) = Opers ((1-Alg A),S) )
assume A3: S = the carrier of (1-Alg B) ; ::_thesis: the charact of (1-Alg B) = Opers ((1-Alg A),S)
reconsider f1 = the charact of (1-Alg B) as PFuncFinSequence of S by A3;
A4: 1-Alg B = UAStr(# (the_sort_of B),(the_charact_of B) #) by MSUALG_1:def_14;
then A5: f1 = the Charact of B by MSUALG_1:def_13;
A6: C is opers_closed by MSUALG_2:def_9;
A7: for n being set
for o being operation of (1-Alg A) st n in dom f1 & o = the charact of (1-Alg A) . n holds
f1 . n = o /. S
proof
let n be set ; ::_thesis: for o being operation of (1-Alg A) st n in dom f1 & o = the charact of (1-Alg A) . n holds
f1 . n = o /. S
let o be operation of (1-Alg A); ::_thesis: ( n in dom f1 & o = the charact of (1-Alg A) . n implies f1 . n = o /. S )
assume that
A8: n in dom f1 and
A9: o = the charact of (1-Alg A) . n ; ::_thesis: f1 . n = o /. S
reconsider y = n as OperSymbol of MS by A5, A8, PARTFUN1:def_2;
o = the Charact of A . y by A2, A9, MSUALG_1:def_13
.= Den (y,A) by MSUALG_1:def_6 ;
then A10: dom o = Args (y,A) by FUNCT_2:def_1
.= (len (the_arity_of y)) -tuples_on (the_sort_of A) by MSUALG_1:6 ;
now__::_thesis:_(_ex_x_being_FinSequence_st_x_in_dom_o_&_(_for_x_being_FinSequence_st_x_in_dom_o_holds_
len_(the_arity_of_y)_=_len_x_)_)
set a = the Element of (len (the_arity_of y)) -tuples_on (the_sort_of A);
the Element of (len (the_arity_of y)) -tuples_on (the_sort_of A) in dom o by A10;
hence ex x being FinSequence st x in dom o ; ::_thesis: for x being FinSequence st x in dom o holds
len (the_arity_of y) = len x
let x be FinSequence; ::_thesis: ( x in dom o implies len (the_arity_of y) = len x )
assume x in dom o ; ::_thesis: len (the_arity_of y) = len x
then ex s being Element of (the_sort_of A) * st
( x = s & len s = len (the_arity_of y) ) by A10;
hence len (the_arity_of y) = len x ; ::_thesis: verum
end;
then A11: arity o = len (the_arity_of y) by MARGREL1:def_25;
S is opers_closed by A3, Th18;
then A12: S is_closed_on o by UNIALG_2:def_4;
A13: C is_closed_on y by A6, MSUALG_2:def_6;
A14: ((C #) * the Arity of MS) . y = Args (y,B) by MSUALG_1:def_4
.= (arity o) -tuples_on S by A4, A3, A11, MSUALG_1:6 ;
f1 . n = the Charact of B . y by A4, MSUALG_1:def_13
.= y /. C by A1, MSUALG_2:def_8
.= (Den (y,A)) | (((C #) * the Arity of MS) . y) by A13, MSUALG_2:def_7
.= ( the Charact of A . y) | (((C #) * the Arity of MS) . y) by MSUALG_1:def_6
.= o | ((arity o) -tuples_on S) by A2, A9, A14, MSUALG_1:def_13 ;
hence f1 . n = o /. S by A12, UNIALG_2:def_5; ::_thesis: verum
end;
dom f1 = the carrier' of MS by A5, PARTFUN1:def_2
.= dom the Charact of A by PARTFUN1:def_2
.= dom the charact of (1-Alg A) by A2, MSUALG_1:def_13 ;
hence the charact of (1-Alg B) = Opers ((1-Alg A),S) by A7, UNIALG_2:def_6; ::_thesis: verum
end;
theorem Th20: :: MSSUBLAT:20
for MS being non void 1 -element segmental ManySortedSign
for A being non-empty MSAlgebra over MS
for B being non-empty MSSubAlgebra of A holds 1-Alg B is SubAlgebra of 1-Alg A
proof
let MS be non void 1 -element segmental ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over MS
for B being non-empty MSSubAlgebra of A holds 1-Alg B is SubAlgebra of 1-Alg A
let A be non-empty MSAlgebra over MS; ::_thesis: for B being non-empty MSSubAlgebra of A holds 1-Alg B is SubAlgebra of 1-Alg A
let B be non-empty MSSubAlgebra of A; ::_thesis: 1-Alg B is SubAlgebra of 1-Alg A
( the carrier of (1-Alg B) is Subset of (1-Alg A) & ( for S being non empty Subset of (1-Alg A) st S = the carrier of (1-Alg B) holds
( the charact of (1-Alg B) = Opers ((1-Alg A),S) & S is opers_closed ) ) ) by Th17, Th18, Th19;
hence 1-Alg B is SubAlgebra of 1-Alg A by UNIALG_2:def_7; ::_thesis: verum
end;
theorem Th21: :: MSSUBLAT:21
for S being non empty non void ManySortedSign
for A, B being MSAlgebra over S holds
( A is MSSubAlgebra of B iff A is MSSubAlgebra of MSAlgebra(# the Sorts of B, the Charact of B #) )
proof
let S be non empty non void ManySortedSign ; ::_thesis: for A, B being MSAlgebra over S holds
( A is MSSubAlgebra of B iff A is MSSubAlgebra of MSAlgebra(# the Sorts of B, the Charact of B #) )
let A, B be MSAlgebra over S; ::_thesis: ( A is MSSubAlgebra of B iff A is MSSubAlgebra of MSAlgebra(# the Sorts of B, the Charact of B #) )
thus ( A is MSSubAlgebra of B implies A is MSSubAlgebra of MSAlgebra(# the Sorts of B, the Charact of B #) ) ::_thesis: ( A is MSSubAlgebra of MSAlgebra(# the Sorts of B, the Charact of B #) implies A is MSSubAlgebra of B )
proof
assume A1: A is MSSubAlgebra of B ; ::_thesis: A is MSSubAlgebra of MSAlgebra(# the Sorts of B, the Charact of B #)
hence the Sorts of A is MSSubset of MSAlgebra(# the Sorts of B, the Charact of B #) by MSUALG_2:def_9; :: according to MSUALG_2:def_9 ::_thesis: for b1 being ManySortedSubset of the Sorts of MSAlgebra(# the Sorts of B, the Charact of B #) holds
( not b1 = the Sorts of A or ( b1 is opers_closed & the Charact of A = Opers (MSAlgebra(# the Sorts of B, the Charact of B #),b1) ) )
thus for BB being MSSubset of MSAlgebra(# the Sorts of B, the Charact of B #) st BB = the Sorts of A holds
( BB is opers_closed & the Charact of A = Opers (MSAlgebra(# the Sorts of B, the Charact of B #),BB) ) ::_thesis: verum
proof
let BB be MSSubset of MSAlgebra(# the Sorts of B, the Charact of B #); ::_thesis: ( BB = the Sorts of A implies ( BB is opers_closed & the Charact of A = Opers (MSAlgebra(# the Sorts of B, the Charact of B #),BB) ) )
assume A2: BB = the Sorts of A ; ::_thesis: ( BB is opers_closed & the Charact of A = Opers (MSAlgebra(# the Sorts of B, the Charact of B #),BB) )
reconsider bb = BB as MSSubset of B ;
A3: bb is opers_closed by A1, A2, MSUALG_2:def_9;
A4: BB is opers_closed
proof
let o be OperSymbol of S; :: according to MSUALG_2:def_6 ::_thesis: BB is_closed_on o
A5: Den (o,B) = the Charact of MSAlgebra(# the Sorts of B, the Charact of B #) . o by MSUALG_1:def_6
.= Den (o,MSAlgebra(# the Sorts of B, the Charact of B #)) by MSUALG_1:def_6 ;
bb is_closed_on o by A3, MSUALG_2:def_6;
then rng ((Den (o,MSAlgebra(# the Sorts of B, the Charact of B #))) | (((BB #) * the Arity of S) . o)) c= (BB * the ResultSort of S) . o by A5, MSUALG_2:def_5;
hence BB is_closed_on o by MSUALG_2:def_5; ::_thesis: verum
end;
for o being set st o in the carrier' of S holds
the Charact of A . o = (Opers (MSAlgebra(# the Sorts of B, the Charact of B #),BB)) . o
proof
let o be set ; ::_thesis: ( o in the carrier' of S implies the Charact of A . o = (Opers (MSAlgebra(# the Sorts of B, the Charact of B #),BB)) . o )
assume o in the carrier' of S ; ::_thesis: the Charact of A . o = (Opers (MSAlgebra(# the Sorts of B, the Charact of B #),BB)) . o
then reconsider o = o as OperSymbol of S ;
A6: Den (o,B) = the Charact of MSAlgebra(# the Sorts of B, the Charact of B #) . o by MSUALG_1:def_6
.= Den (o,MSAlgebra(# the Sorts of B, the Charact of B #)) by MSUALG_1:def_6 ;
A7: bb is_closed_on o by A3, MSUALG_2:def_6;
A8: BB is_closed_on o by A4, MSUALG_2:def_6;
(Opers (B,bb)) . o = o /. bb by MSUALG_2:def_8
.= (Den (o,MSAlgebra(# the Sorts of B, the Charact of B #))) | (((BB #) * the Arity of S) . o) by A6, A7, MSUALG_2:def_7
.= o /. BB by A8, MSUALG_2:def_7
.= (Opers (MSAlgebra(# the Sorts of B, the Charact of B #),BB)) . o by MSUALG_2:def_8 ;
hence the Charact of A . o = (Opers (MSAlgebra(# the Sorts of B, the Charact of B #),BB)) . o by A1, A2, MSUALG_2:def_9; ::_thesis: verum
end;
hence ( BB is opers_closed & the Charact of A = Opers (MSAlgebra(# the Sorts of B, the Charact of B #),BB) ) by A4, PBOOLE:3; ::_thesis: verum
end;
end;
assume A9: A is MSSubAlgebra of MSAlgebra(# the Sorts of B, the Charact of B #) ; ::_thesis: A is MSSubAlgebra of B
hence the Sorts of A is MSSubset of B by MSUALG_2:def_9; :: according to MSUALG_2:def_9 ::_thesis: for b1 being ManySortedSubset of the Sorts of B holds
( not b1 = the Sorts of A or ( b1 is opers_closed & the Charact of A = Opers (B,b1) ) )
let C be MSSubset of B; ::_thesis: ( not C = the Sorts of A or ( C is opers_closed & the Charact of A = Opers (B,C) ) )
assume A10: C = the Sorts of A ; ::_thesis: ( C is opers_closed & the Charact of A = Opers (B,C) )
reconsider CC = C as MSSubset of MSAlgebra(# the Sorts of B, the Charact of B #) ;
A11: CC is opers_closed by A9, A10, MSUALG_2:def_9;
A12: C is opers_closed
proof
let o be OperSymbol of S; :: according to MSUALG_2:def_6 ::_thesis: C is_closed_on o
A13: Den (o,B) = the Charact of MSAlgebra(# the Sorts of B, the Charact of B #) . o by MSUALG_1:def_6
.= Den (o,MSAlgebra(# the Sorts of B, the Charact of B #)) by MSUALG_1:def_6 ;
CC is_closed_on o by A11, MSUALG_2:def_6;
then rng ((Den (o,B)) | (((C #) * the Arity of S) . o)) c= (C * the ResultSort of S) . o by A13, MSUALG_2:def_5;
hence C is_closed_on o by MSUALG_2:def_5; ::_thesis: verum
end;
for o being set st o in the carrier' of S holds
the Charact of A . o = (Opers (B,C)) . o
proof
let o be set ; ::_thesis: ( o in the carrier' of S implies the Charact of A . o = (Opers (B,C)) . o )
assume o in the carrier' of S ; ::_thesis: the Charact of A . o = (Opers (B,C)) . o
then reconsider o = o as OperSymbol of S ;
A14: Den (o,B) = the Charact of MSAlgebra(# the Sorts of B, the Charact of B #) . o by MSUALG_1:def_6
.= Den (o,MSAlgebra(# the Sorts of B, the Charact of B #)) by MSUALG_1:def_6 ;
A15: CC is_closed_on o by A11, MSUALG_2:def_6;
A16: C is_closed_on o by A12, MSUALG_2:def_6;
(Opers (MSAlgebra(# the Sorts of B, the Charact of B #),CC)) . o = o /. CC by MSUALG_2:def_8
.= (Den (o,B)) | (((C #) * the Arity of S) . o) by A14, A15, MSUALG_2:def_7
.= o /. C by A16, MSUALG_2:def_7
.= (Opers (B,C)) . o by MSUALG_2:def_8 ;
hence the Charact of A . o = (Opers (B,C)) . o by A9, A10, MSUALG_2:def_9; ::_thesis: verum
end;
hence ( C is opers_closed & the Charact of A = Opers (B,C) ) by A12, PBOOLE:3; ::_thesis: verum
end;
theorem :: MSSUBLAT:22
for A, B being Universal_Algebra holds
( signature A = signature B iff MSSign A = MSSign B )
proof
A1: for A, B being Universal_Algebra st MSSign A = MSSign B holds
signature A = signature B
proof
let A, B be Universal_Algebra; ::_thesis: ( MSSign A = MSSign B implies signature A = signature B )
reconsider ff1 = (*--> 0) * (signature A) as Function of (dom (signature A)),({0} *) by MSUALG_1:2;
reconsider gg1 = (*--> 0) * (signature B) as Function of (dom (signature B)),({0} *) by MSUALG_1:2;
A2: ( MSSign A = ManySortedSign(# {0},(dom (signature A)),ff1,((dom (signature A)) --> z) #) & MSSign B = ManySortedSign(# {0},(dom (signature B)),gg1,((dom (signature B)) --> z) #) ) by MSUALG_1:10;
assume A3: MSSign A = MSSign B ; ::_thesis: signature A = signature B
now__::_thesis:_for_i_being_Nat_st_i_in_dom_(signature_A)_holds_
(signature_A)_._i_=_(signature_B)_._i
let i be Nat; ::_thesis: ( i in dom (signature A) implies (signature A) . i = (signature B) . i )
assume A4: i in dom (signature A) ; ::_thesis: (signature A) . i = (signature B) . i
then reconsider k = (signature A) . i as Element of NAT by PARTFUN1:4;
A5: i in dom ((*--> 0) * (signature A)) by A4, FINSEQ_3:120;
then A6: (*--> 0) . ((signature B) . i) = ((*--> 0) * (signature A)) . i by A3, A2, FINSEQ_3:120
.= (*--> 0) . ((signature A) . i) by A5, FINSEQ_3:120 ;
reconsider m = (signature B) . i as Element of NAT by A3, A2, A4, PARTFUN1:4;
reconsider q = (*--> 0) . m as FinSequence ;
reconsider p = (*--> 0) . k as FinSequence ;
thus (signature A) . i = len p by Th6
.= len q by A6
.= (signature B) . i by Th6 ; ::_thesis: verum
end;
hence signature A = signature B by A3, A2, FINSEQ_1:13; ::_thesis: verum
end;
for A, B being Universal_Algebra st signature A = signature B holds
MSSign A = MSSign B
proof
let A, B be Universal_Algebra; ::_thesis: ( signature A = signature B implies MSSign A = MSSign B )
assume signature A = signature B ; ::_thesis: MSSign A = MSSign B
then A,B are_similar by UNIALG_2:def_1;
hence MSSign A = MSSign B by MSUHOM_1:10; ::_thesis: verum
end;
hence for A, B being Universal_Algebra holds
( signature A = signature B iff MSSign A = MSSign B ) by A1; ::_thesis: verum
end;
theorem Th23: :: MSSUBLAT:23
for MS being non void 1 -element segmental ManySortedSign
for A being non-empty MSAlgebra over MS st the carrier of MS = {0} holds
MSSign (1-Alg A) = ManySortedSign(# the carrier of MS, the carrier' of MS, the Arity of MS, the ResultSort of MS #)
proof
let MS be non void 1 -element segmental ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over MS st the carrier of MS = {0} holds
MSSign (1-Alg A) = ManySortedSign(# the carrier of MS, the carrier' of MS, the Arity of MS, the ResultSort of MS #)
let A be non-empty MSAlgebra over MS; ::_thesis: ( the carrier of MS = {0} implies MSSign (1-Alg A) = ManySortedSign(# the carrier of MS, the carrier' of MS, the Arity of MS, the ResultSort of MS #) )
reconsider ff1 = (*--> 0) * (signature (1-Alg A)) as Function of (dom (signature (1-Alg A))),({0} *) by MSUALG_1:2;
A1: MSSign (1-Alg A) = ManySortedSign(# {0},(dom (signature (1-Alg A))),ff1,((dom (signature (1-Alg A))) --> z) #) by MSUALG_1:10;
dom the ResultSort of MS = the carrier' of MS by FUNCT_2:def_1;
then A2: rng the ResultSort of MS <> {} by RELAT_1:42;
consider k being Nat such that
A3: the carrier' of MS = Seg k by MSUALG_1:def_7;
A4: 1-Alg A = UAStr(# (the_sort_of A),(the_charact_of A) #) by MSUALG_1:def_14;
A5: len (signature (1-Alg A)) = len the charact of (1-Alg A) by UNIALG_1:def_4;
then A6: dom (signature (1-Alg A)) = dom the charact of (1-Alg A) by FINSEQ_3:29
.= dom the Charact of A by A4, MSUALG_1:def_13
.= the carrier' of MS by PARTFUN1:def_2 ;
then A7: the carrier' of MS = dom ff1 by FUNCT_2:def_1;
assume A8: the carrier of MS = {0} ; ::_thesis: MSSign (1-Alg A) = ManySortedSign(# the carrier of MS, the carrier' of MS, the Arity of MS, the ResultSort of MS #)
A9: for x being set st x in the carrier' of MS holds
((*--> 0) * (signature (1-Alg A))) . x = the Arity of MS . x
proof
let x be set ; ::_thesis: ( x in the carrier' of MS implies ((*--> 0) * (signature (1-Alg A))) . x = the Arity of MS . x )
assume x in the carrier' of MS ; ::_thesis: ((*--> 0) * (signature (1-Alg A))) . x = the Arity of MS . x
then reconsider x = x as OperSymbol of MS ;
x in Seg k by A3;
then reconsider n = x as Nat ;
n in dom (signature (1-Alg A)) by A6;
then A10: n in dom the charact of (1-Alg A) by A5, FINSEQ_3:29;
then reconsider h = the charact of (1-Alg A) . n as PartFunc of ( the carrier of (1-Alg A) *), the carrier of (1-Alg A) by UNIALG_1:1;
reconsider h = h as non empty homogeneous quasi_total PartFunc of ( the carrier of (1-Alg A) *), the carrier of (1-Alg A) by A10, MARGREL1:def_24;
set aa = the Element of dom h;
set ah = arity h;
dom h c= the carrier of (1-Alg A) * by RELAT_1:def_18;
then the Element of dom h in the carrier of (1-Alg A) * by TARSKI:def_3;
then reconsider bb = the Element of dom h as FinSequence of the carrier of (1-Alg A) by FINSEQ_1:def_11;
A11: bb in dom h ;
h = the Charact of A . x by A4, MSUALG_1:def_13
.= Den (x,A) by MSUALG_1:def_6 ;
then bb in Args (x,A) by A11, FUNCT_2:def_1;
then bb in (len (the_arity_of x)) -tuples_on (the_sort_of A) by MSUALG_1:6;
then A12: len (the_arity_of x) = len bb by CARD_1:def_7
.= arity h by MARGREL1:def_25 ;
((*--> 0) * (signature (1-Alg A))) . x = (*--> 0) . ((signature (1-Alg A)) . x) by A6, FUNCT_1:13
.= (*--> 0) . (arity h) by A6, UNIALG_1:def_4
.= (arity h) |-> 0 by FINSEQ_2:def_6
.= the_arity_of x by A8, A12, Th5
.= the Arity of MS . x by MSUALG_1:def_1 ;
hence ((*--> 0) * (signature (1-Alg A))) . x = the Arity of MS . x ; ::_thesis: verum
end;
rng the ResultSort of MS c= {0} by A8, RELAT_1:def_19;
then ( the carrier' of MS = dom the ResultSort of MS & rng the ResultSort of MS = {0} ) by A2, FUNCT_2:def_1, ZFMISC_1:33;
then ( the carrier' of MS = dom the Arity of MS & the ResultSort of (MSSign (1-Alg A)) = the ResultSort of MS ) by A1, A6, FUNCOP_1:9, FUNCT_2:def_1;
hence MSSign (1-Alg A) = ManySortedSign(# the carrier of MS, the carrier' of MS, the Arity of MS, the ResultSort of MS #) by A8, A1, A6, A7, A9, FUNCT_1:2; ::_thesis: verum
end;
theorem Th24: :: MSSUBLAT:24
for MS being non void 1 -element segmental ManySortedSign
for A, B being non-empty MSAlgebra over MS st 1-Alg A = 1-Alg B holds
MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #)
proof
let MS be non void 1 -element segmental ManySortedSign ; ::_thesis: for A, B being non-empty MSAlgebra over MS st 1-Alg A = 1-Alg B holds
MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #)
let A, B be non-empty MSAlgebra over MS; ::_thesis: ( 1-Alg A = 1-Alg B implies MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #) )
assume A1: 1-Alg A = 1-Alg B ; ::_thesis: MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #)
A2: 1-Alg B = UAStr(# (the_sort_of B),(the_charact_of B) #) by MSUALG_1:def_14;
A3: 1-Alg A = UAStr(# (the_sort_of A),(the_charact_of A) #) by MSUALG_1:def_14;
A4: now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_MS_holds_
the_Sorts_of_A_._i_=_the_Sorts_of_B_._i
let i be set ; ::_thesis: ( i in the carrier of MS implies the Sorts of A . i = the Sorts of B . i )
assume A5: i in the carrier of MS ; ::_thesis: the Sorts of A . i = the Sorts of B . i
A6: ex c being Component of the Sorts of B st the Sorts of B . i = c
proof
reconsider c = the Sorts of B . i as Component of the Sorts of B by A5, PBOOLE:139;
take c ; ::_thesis: the Sorts of B . i = c
thus the Sorts of B . i = c ; ::_thesis: verum
end;
ex c being Component of the Sorts of A st the Sorts of A . i = c
proof
reconsider c = the Sorts of A . i as Component of the Sorts of A by A5, PBOOLE:139;
take c ; ::_thesis: the Sorts of A . i = c
thus the Sorts of A . i = c ; ::_thesis: verum
end;
then the Sorts of A . i = the_sort_of B by A1, A3, A2, MSUALG_1:def_12
.= the Sorts of B . i by A6, MSUALG_1:def_12 ;
hence the Sorts of A . i = the Sorts of B . i ; ::_thesis: verum
end;
the Charact of A = the charact of (1-Alg A) by A3, MSUALG_1:def_13
.= the Charact of B by A1, A2, MSUALG_1:def_13 ;
hence MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #) by A4, PBOOLE:3; ::_thesis: verum
end;
theorem :: MSSUBLAT:25
for MS being non void 1 -element segmental ManySortedSign
for A being non-empty MSAlgebra over MS st the carrier of MS = {0} holds
the Sorts of A = the Sorts of (MSAlg (1-Alg A))
proof
let MS be non void 1 -element segmental ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over MS st the carrier of MS = {0} holds
the Sorts of A = the Sorts of (MSAlg (1-Alg A))
let A be non-empty MSAlgebra over MS; ::_thesis: ( the carrier of MS = {0} implies the Sorts of A = the Sorts of (MSAlg (1-Alg A)) )
assume A1: the carrier of MS = {0} ; ::_thesis: the Sorts of A = the Sorts of (MSAlg (1-Alg A))
A2: now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_MS_holds_
the_Sorts_of_A_._i_=_({0}_-->_(the_sort_of_A))_._i
let i be set ; ::_thesis: ( i in the carrier of MS implies the Sorts of A . i = ({0} --> (the_sort_of A)) . i )
assume A3: i in the carrier of MS ; ::_thesis: the Sorts of A . i = ({0} --> (the_sort_of A)) . i
A4: ex c being Component of the Sorts of A st the Sorts of A . i = c
proof
reconsider c = the Sorts of A . i as Component of the Sorts of A by A3, PBOOLE:139;
take c ; ::_thesis: the Sorts of A . i = c
thus the Sorts of A . i = c ; ::_thesis: verum
end;
({0} --> (the_sort_of A)) . i = the_sort_of A by A1, A3, FUNCOP_1:7;
hence the Sorts of A . i = ({0} --> (the_sort_of A)) . i by A4, MSUALG_1:def_12; ::_thesis: verum
end;
1-Alg A = UAStr(# (the_sort_of A),(the_charact_of A) #) by MSUALG_1:def_14;
then A5: ( MSAlg (1-Alg A) = MSAlgebra(# (MSSorts (1-Alg A)),(MSCharact (1-Alg A)) #) & MSSorts (1-Alg A) = 0 .--> (the_sort_of A) ) by MSUALG_1:def_9, MSUALG_1:def_11;
{0} --> (the_sort_of A) is ManySortedSet of the carrier of MS by A1;
hence the Sorts of A = the Sorts of (MSAlg (1-Alg A)) by A5, A2, PBOOLE:3; ::_thesis: verum
end;
theorem Th26: :: MSSUBLAT:26
for MS being non void 1 -element segmental ManySortedSign
for A being non-empty MSAlgebra over MS st the carrier of MS = {0} holds
MSAlg (1-Alg A) = MSAlgebra(# the Sorts of A, the Charact of A #)
proof
let MS be non void 1 -element segmental ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over MS st the carrier of MS = {0} holds
MSAlg (1-Alg A) = MSAlgebra(# the Sorts of A, the Charact of A #)
let A be non-empty MSAlgebra over MS; ::_thesis: ( the carrier of MS = {0} implies MSAlg (1-Alg A) = MSAlgebra(# the Sorts of A, the Charact of A #) )
reconsider c = the_sort_of (MSAlg (1-Alg A)) as Component of the Sorts of (MSAlg (1-Alg A)) by MSUALG_1:def_12;
assume the carrier of MS = {0} ; ::_thesis: MSAlg (1-Alg A) = MSAlgebra(# the Sorts of A, the Charact of A #)
then MSSign (1-Alg A) = ManySortedSign(# the carrier of MS, the carrier' of MS, the Arity of MS, the ResultSort of MS #) by Th23;
then reconsider M1A = MSAlg (1-Alg A) as strict MSAlgebra over MS ;
reconsider M1A = M1A as strict non-empty MSAlgebra over MS by MSUALG_1:def_3;
A1: 1-Alg M1A = UAStr(# (the_sort_of M1A),(the_charact_of M1A) #) by MSUALG_1:def_14;
reconsider c = c as Component of the Sorts of M1A ;
A2: 1-Alg (MSAlg (1-Alg A)) = UAStr(# (the_sort_of (MSAlg (1-Alg A))),(the_charact_of (MSAlg (1-Alg A))) #) by MSUALG_1:def_14;
then A3: the charact of (1-Alg A) = the_charact_of (MSAlg (1-Alg A)) by MSUALG_1:9
.= the Charact of M1A by MSUALG_1:def_13
.= the charact of (1-Alg M1A) by A1, MSUALG_1:def_13 ;
c = the_sort_of M1A by MSUALG_1:def_12;
then the carrier of (1-Alg A) = the carrier of (1-Alg M1A) by A2, A1, MSUALG_1:9;
hence MSAlg (1-Alg A) = MSAlgebra(# the Sorts of A, the Charact of A #) by A3, Th24; ::_thesis: verum
end;
theorem :: MSSUBLAT:27
for A being Universal_Algebra
for B being strict non-empty MSSubAlgebra of MSAlg A st the carrier of (MSSign A) = {0} holds
1-Alg B is SubAlgebra of A
proof
let A be Universal_Algebra; ::_thesis: for B being strict non-empty MSSubAlgebra of MSAlg A st the carrier of (MSSign A) = {0} holds
1-Alg B is SubAlgebra of A
let B be strict non-empty MSSubAlgebra of MSAlg A; ::_thesis: ( the carrier of (MSSign A) = {0} implies 1-Alg B is SubAlgebra of A )
assume the carrier of (MSSign A) = {0} ; ::_thesis: 1-Alg B is SubAlgebra of A
then MSAlg (1-Alg B) = MSAlgebra(# the Sorts of B, the Charact of B #) by Th26;
hence 1-Alg B is SubAlgebra of A by Th16; ::_thesis: verum
end;
begin
theorem Th28: :: MSSUBLAT:28
for A being Universal_Algebra
for a1, b1 being strict SubAlgebra of A
for a2, b2 being strict non-empty MSSubAlgebra of MSAlg A st a2 = MSAlg a1 & b2 = MSAlg b1 holds
the Sorts of a2 \/ the Sorts of b2 = 0 .--> ( the carrier of a1 \/ the carrier of b1)
proof
let A be Universal_Algebra; ::_thesis: for a1, b1 being strict SubAlgebra of A
for a2, b2 being strict non-empty MSSubAlgebra of MSAlg A st a2 = MSAlg a1 & b2 = MSAlg b1 holds
the Sorts of a2 \/ the Sorts of b2 = 0 .--> ( the carrier of a1 \/ the carrier of b1)
let a1, b1 be strict SubAlgebra of A; ::_thesis: for a2, b2 being strict non-empty MSSubAlgebra of MSAlg A st a2 = MSAlg a1 & b2 = MSAlg b1 holds
the Sorts of a2 \/ the Sorts of b2 = 0 .--> ( the carrier of a1 \/ the carrier of b1)
let a2, b2 be strict non-empty MSSubAlgebra of MSAlg A; ::_thesis: ( a2 = MSAlg a1 & b2 = MSAlg b1 implies the Sorts of a2 \/ the Sorts of b2 = 0 .--> ( the carrier of a1 \/ the carrier of b1) )
assume that
A1: a2 = MSAlg a1 and
A2: b2 = MSAlg b1 ; ::_thesis: the Sorts of a2 \/ the Sorts of b2 = 0 .--> ( the carrier of a1 \/ the carrier of b1)
a2 = MSAlgebra(# (MSSorts a1),(MSCharact a1) #) by A1, MSUALG_1:def_11;
then A3: the Sorts of a2 = 0 .--> the carrier of a1 by MSUALG_1:def_9;
reconsider ff1 = (*--> 0) * (signature A) as Function of (dom (signature A)),({0} *) by MSUALG_1:2;
A4: MSSign A = ManySortedSign(# {0},(dom (signature A)),ff1,((dom (signature A)) --> z) #) by MSUALG_1:10;
then reconsider W = 0 .--> ( the carrier of a1 \/ the carrier of b1) as ManySortedSet of the carrier of (MSSign A) ;
A5: b2 = MSAlgebra(# (MSSorts b1),(MSCharact b1) #) by A2, MSUALG_1:def_11;
now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_(MSSign_A)_holds_
W_._x_=_(_the_Sorts_of_a2_._x)_\/_(_the_Sorts_of_b2_._x)
let x be set ; ::_thesis: ( x in the carrier of (MSSign A) implies W . x = ( the Sorts of a2 . x) \/ ( the Sorts of b2 . x) )
assume A6: x in the carrier of (MSSign A) ; ::_thesis: W . x = ( the Sorts of a2 . x) \/ ( the Sorts of b2 . x)
then A7: x = 0 by A4, TARSKI:def_1;
W . x = (0 .--> ( the carrier of a1 \/ the carrier of b1)) . 0 by A4, A6, TARSKI:def_1
.= the carrier of a1 \/ the carrier of b1 by FUNCOP_1:72
.= ((0 .--> the carrier of a1) . 0) \/ the carrier of b1 by FUNCOP_1:72
.= ((0 .--> the carrier of a1) . 0) \/ ((0 .--> the carrier of b1) . 0) by FUNCOP_1:72
.= ( the Sorts of a2 . x) \/ ( the Sorts of b2 . x) by A3, A5, A7, MSUALG_1:def_9 ;
hence W . x = ( the Sorts of a2 . x) \/ ( the Sorts of b2 . x) ; ::_thesis: verum
end;
hence the Sorts of a2 \/ the Sorts of b2 = 0 .--> ( the carrier of a1 \/ the carrier of b1) by PBOOLE:def_4; ::_thesis: verum
end;
theorem Th29: :: MSSUBLAT:29
for A being Universal_Algebra
for a1, b1 being strict non-empty SubAlgebra of A
for a2, b2 being strict non-empty MSSubAlgebra of MSAlg A st a2 = MSAlg a1 & b2 = MSAlg b1 holds
the Sorts of a2 /\ the Sorts of b2 = 0 .--> ( the carrier of a1 /\ the carrier of b1)
proof
let A be Universal_Algebra; ::_thesis: for a1, b1 being strict non-empty SubAlgebra of A
for a2, b2 being strict non-empty MSSubAlgebra of MSAlg A st a2 = MSAlg a1 & b2 = MSAlg b1 holds
the Sorts of a2 /\ the Sorts of b2 = 0 .--> ( the carrier of a1 /\ the carrier of b1)
let a1, b1 be strict non-empty SubAlgebra of A; ::_thesis: for a2, b2 being strict non-empty MSSubAlgebra of MSAlg A st a2 = MSAlg a1 & b2 = MSAlg b1 holds
the Sorts of a2 /\ the Sorts of b2 = 0 .--> ( the carrier of a1 /\ the carrier of b1)
let a2, b2 be strict non-empty MSSubAlgebra of MSAlg A; ::_thesis: ( a2 = MSAlg a1 & b2 = MSAlg b1 implies the Sorts of a2 /\ the Sorts of b2 = 0 .--> ( the carrier of a1 /\ the carrier of b1) )
assume that
A1: a2 = MSAlg a1 and
A2: b2 = MSAlg b1 ; ::_thesis: the Sorts of a2 /\ the Sorts of b2 = 0 .--> ( the carrier of a1 /\ the carrier of b1)
a2 = MSAlgebra(# (MSSorts a1),(MSCharact a1) #) by A1, MSUALG_1:def_11;
then A3: the Sorts of a2 = 0 .--> the carrier of a1 by MSUALG_1:def_9;
reconsider ff1 = (*--> 0) * (signature A) as Function of (dom (signature A)),({0} *) by MSUALG_1:2;
A4: MSSign A = ManySortedSign(# {0},(dom (signature A)),ff1,((dom (signature A)) --> z) #) by MSUALG_1:10;
then reconsider W = 0 .--> ( the carrier of a1 /\ the carrier of b1) as ManySortedSet of the carrier of (MSSign A) ;
A5: b2 = MSAlgebra(# (MSSorts b1),(MSCharact b1) #) by A2, MSUALG_1:def_11;
now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_(MSSign_A)_holds_
W_._x_=_(_the_Sorts_of_a2_._x)_/\_(_the_Sorts_of_b2_._x)
let x be set ; ::_thesis: ( x in the carrier of (MSSign A) implies W . x = ( the Sorts of a2 . x) /\ ( the Sorts of b2 . x) )
assume x in the carrier of (MSSign A) ; ::_thesis: W . x = ( the Sorts of a2 . x) /\ ( the Sorts of b2 . x)
then A6: x = 0 by A4, TARSKI:def_1;
then W . x = the carrier of a1 /\ the carrier of b1 by FUNCOP_1:72
.= ((0 .--> the carrier of a1) . 0) /\ the carrier of b1 by FUNCOP_1:72
.= ((0 .--> the carrier of a1) . 0) /\ ((0 .--> the carrier of b1) . 0) by FUNCOP_1:72
.= ( the Sorts of a2 . x) /\ ( the Sorts of b2 . x) by A3, A5, A6, MSUALG_1:def_9 ;
hence W . x = ( the Sorts of a2 . x) /\ ( the Sorts of b2 . x) ; ::_thesis: verum
end;
hence the Sorts of a2 /\ the Sorts of b2 = 0 .--> ( the carrier of a1 /\ the carrier of b1) by PBOOLE:def_5; ::_thesis: verum
end;
theorem Th30: :: MSSUBLAT:30
for A being strict Universal_Algebra
for a1, b1 being strict non-empty SubAlgebra of A
for a2, b2 being strict non-empty MSSubAlgebra of MSAlg A st a2 = MSAlg a1 & b2 = MSAlg b1 holds
MSAlg (a1 "\/" b1) = a2 "\/" b2
proof
let A be strict Universal_Algebra; ::_thesis: for a1, b1 being strict non-empty SubAlgebra of A
for a2, b2 being strict non-empty MSSubAlgebra of MSAlg A st a2 = MSAlg a1 & b2 = MSAlg b1 holds
MSAlg (a1 "\/" b1) = a2 "\/" b2
let a1, b1 be strict non-empty SubAlgebra of A; ::_thesis: for a2, b2 being strict non-empty MSSubAlgebra of MSAlg A st a2 = MSAlg a1 & b2 = MSAlg b1 holds
MSAlg (a1 "\/" b1) = a2 "\/" b2
reconsider MSA = MSAlg (a1 "\/" b1) as MSSubAlgebra of MSAlg A by Th12;
let a2, b2 be strict non-empty MSSubAlgebra of MSAlg A; ::_thesis: ( a2 = MSAlg a1 & b2 = MSAlg b1 implies MSAlg (a1 "\/" b1) = a2 "\/" b2 )
assume that
A1: a2 = MSAlg a1 and
A2: b2 = MSAlg b1 ; ::_thesis: MSAlg (a1 "\/" b1) = a2 "\/" b2
MSSign (a1 "\/" b1) = MSSign A by Th7;
then reconsider MSA = MSA as strict non-empty MSSubAlgebra of MSAlg A ;
for B being MSSubset of (MSAlg A) st B = the Sorts of a2 \/ the Sorts of b2 holds
MSA = GenMSAlg B
proof
( the carrier of a1 is Subset of A & the carrier of b1 is Subset of A ) by UNIALG_2:def_7;
then reconsider K = the carrier of a1 \/ the carrier of b1 as non empty Subset of A by XBOOLE_1:8;
reconsider ff1 = (*--> 0) * (signature A) as Function of (dom (signature A)),({0} *) by MSUALG_1:2;
set X = MSA;
reconsider M1 = the Sorts of MSA as ManySortedSet of the carrier of (MSSign A) ;
A3: MSSign A = ManySortedSign(# {0},(dom (signature A)),ff1,((dom (signature A)) --> z) #) by MSUALG_1:10;
then reconsider x = 0 as Element of (MSSign A) ;
let B be MSSubset of (MSAlg A); ::_thesis: ( B = the Sorts of a2 \/ the Sorts of b2 implies MSA = GenMSAlg B )
assume A4: B = the Sorts of a2 \/ the Sorts of b2 ; ::_thesis: MSA = GenMSAlg B
A5: for U1 being MSSubAlgebra of MSAlg A st B is MSSubset of U1 holds
MSA is MSSubAlgebra of U1
proof
let U1 be MSSubAlgebra of MSAlg A; ::_thesis: ( B is MSSubset of U1 implies MSA is MSSubAlgebra of U1 )
assume A6: B is MSSubset of U1 ; ::_thesis: MSA is MSSubAlgebra of U1
percases ( U1 is non-empty or not U1 is non-empty ) ;
suppose U1 is non-empty ; ::_thesis: MSA is MSSubAlgebra of U1
then reconsider U11 = U1 as non-empty MSSubAlgebra of MSAlg A ;
A7: 1-Alg U11 is SubAlgebra of 1-Alg (MSAlg A) by Th20;
then reconsider A1 = 1-Alg U11 as strict SubAlgebra of A by MSUALG_1:9;
B c= the Sorts of U11 by A6, PBOOLE:def_18;
then A8: B . x c= the Sorts of U11 . x by PBOOLE:def_2;
( MSAlgebra(# the Sorts of U11, the Charact of U11 #) = MSAlg (1-Alg U11) & MSAlg (1-Alg U11) = MSAlgebra(# (MSSorts (1-Alg U11)),(MSCharact (1-Alg U11)) #) ) by A3, Th26, MSUALG_1:def_11;
then A9: the Sorts of U11 . 0 = (0 .--> the carrier of (1-Alg U11)) . 0 by MSUALG_1:def_9;
B . 0 = (0 .--> K) . 0 by A1, A2, A4, Th28
.= K by FUNCOP_1:72 ;
then the carrier of a1 \/ the carrier of b1 c= the carrier of A1 by A8, A9, FUNCOP_1:72;
then GenUnivAlg K is SubAlgebra of 1-Alg U11 by UNIALG_2:def_12;
then a1 "\/" b1 is SubAlgebra of 1-Alg U11 by UNIALG_2:def_13;
then A10: MSA is MSSubAlgebra of MSAlg (1-Alg U11) by Th12;
1-Alg U11 is SubAlgebra of A by A7, MSUALG_1:9;
then MSSign A = MSSign (1-Alg U11) by Th7;
then MSA is MSSubAlgebra of MSAlgebra(# the Sorts of U11, the Charact of U11 #) by A3, A10, Th26;
hence MSA is MSSubAlgebra of U1 by Th21; ::_thesis: verum
end;
suppose not U1 is non-empty ; ::_thesis: MSA is MSSubAlgebra of U1
then the Sorts of U1 is V2() by MSUALG_1:def_3;
then A11: ex i being set st
( i in the carrier of (MSSign A) & the Sorts of U1 . i is empty ) by PBOOLE:def_13;
reconsider 0a1 = 0 .--> the carrier of a1 as ManySortedSet of the carrier of (MSSign A) by A3;
set e = the Element of a1;
B c= the Sorts of U1 by A6, PBOOLE:def_18;
then A12: B . x c= the Sorts of U1 . x by PBOOLE:def_2;
a2 = MSAlgebra(# (MSSorts a1),(MSCharact a1) #) by A1, MSUALG_1:def_11;
then B = 0a1 \/ the Sorts of b2 by A4, MSUALG_1:def_9;
then A13: B . x = (0a1 . x) \/ ( the Sorts of b2 . x) by PBOOLE:def_4;
x in {0} by TARSKI:def_1;
then 0a1 . x = the carrier of a1 by FUNCOP_1:7;
then the Element of a1 in B . x by A13, XBOOLE_0:def_3;
hence MSA is MSSubAlgebra of U1 by A3, A11, A12, TARSKI:def_1; ::_thesis: verum
end;
end;
end;
MSA = MSAlgebra(# (MSSorts (a1 "\/" b1)),(MSCharact (a1 "\/" b1)) #) by MSUALG_1:def_11;
then A14: the Sorts of MSA = 0 .--> the carrier of (a1 "\/" b1) by MSUALG_1:def_9;
the Sorts of a2 \/ the Sorts of b2 c= M1
proof
let x be set ; :: according to PBOOLE:def_2 ::_thesis: ( not x in the carrier of (MSSign A) or ( the Sorts of a2 \/ the Sorts of b2) . x c= M1 . x )
A15: a1 "\/" b1 = GenUnivAlg K by UNIALG_2:def_13;
assume A16: x in the carrier of (MSSign A) ; ::_thesis: ( the Sorts of a2 \/ the Sorts of b2) . x c= M1 . x
then A17: M1 . x = (0 .--> the carrier of (a1 "\/" b1)) . 0 by A14, A3, TARSKI:def_1
.= the carrier of (a1 "\/" b1) by FUNCOP_1:72 ;
( the Sorts of a2 \/ the Sorts of b2) . x = ( the Sorts of a2 \/ the Sorts of b2) . 0 by A3, A16, TARSKI:def_1
.= (0 .--> ( the carrier of a1 \/ the carrier of b1)) . 0 by A1, A2, Th28
.= the carrier of a1 \/ the carrier of b1 by FUNCOP_1:72 ;
hence ( the Sorts of a2 \/ the Sorts of b2) . x c= M1 . x by A17, A15, UNIALG_2:def_12; ::_thesis: verum
end;
then B is MSSubset of MSA by A4, PBOOLE:def_18;
hence MSA = GenMSAlg B by A5, MSUALG_2:def_17; ::_thesis: verum
end;
hence MSAlg (a1 "\/" b1) = a2 "\/" b2 by MSUALG_2:def_18; ::_thesis: verum
end;
registration
let A be with_const_op Universal_Algebra;
cluster MSSign A -> all-with_const_op ;
coherence
( not MSSign A is void & MSSign A is strict & MSSign A is segmental & MSSign A is trivial & MSSign A is all-with_const_op )
proof
reconsider ff1 = (*--> 0) * (signature A) as Function of (dom (signature A)),({0} *) by MSUALG_1:2;
A1: MSSign A = ManySortedSign(# {0},(dom (signature A)),ff1,((dom (signature A)) --> z) #) by MSUALG_1:10;
MSSign A is all-with_const_op
proof
let s be SortSymbol of (MSSign A); :: according to MSUALG_2:def_2 ::_thesis: s is with_const_op
consider OO being operation of A such that
A2: arity OO = 0 by UNIALG_2:def_11;
Seg (len the charact of A) = dom the charact of A by FINSEQ_1:def_3;
then consider i being Nat such that
A3: i in Seg (len the charact of A) and
A4: the charact of A . i = OO by FINSEQ_2:10;
A5: len (signature A) = len the charact of A by UNIALG_1:def_4;
then A6: i in dom (signature A) by A3, FINSEQ_1:def_3;
reconsider i = i as OperSymbol of (MSSign A) by A1, A3, A5, FINSEQ_1:def_3;
take i ; :: according to MSUALG_2:def_1 ::_thesis: ( the Arity of (MSSign A) . i = {} & the ResultSort of (MSSign A) . i = s )
(*--> 0) . ((signature A) . i) = (*--> 0) . 0 by A2, A4, A6, UNIALG_1:def_4
.= {} by Th1 ;
hence the Arity of (MSSign A) . i = {} by A1, FUNCT_1:13; ::_thesis: the ResultSort of (MSSign A) . i = s
the ResultSort of (MSSign A) . i = 0 by A1, TARSKI:def_1;
hence the ResultSort of (MSSign A) . i = s by A1, TARSKI:def_1; ::_thesis: verum
end;
hence ( not MSSign A is void & MSSign A is strict & MSSign A is segmental & MSSign A is trivial & MSSign A is all-with_const_op ) ; ::_thesis: verum
end;
end;
theorem Th31: :: MSSUBLAT:31
for A being with_const_op Universal_Algebra
for a1, b1 being strict non-empty SubAlgebra of A
for a2, b2 being strict non-empty MSSubAlgebra of MSAlg A st a2 = MSAlg a1 & b2 = MSAlg b1 holds
MSAlg (a1 /\ b1) = a2 /\ b2
proof
let A be with_const_op Universal_Algebra; ::_thesis: for a1, b1 being strict non-empty SubAlgebra of A
for a2, b2 being strict non-empty MSSubAlgebra of MSAlg A st a2 = MSAlg a1 & b2 = MSAlg b1 holds
MSAlg (a1 /\ b1) = a2 /\ b2
let a1, b1 be strict non-empty SubAlgebra of A; ::_thesis: for a2, b2 being strict non-empty MSSubAlgebra of MSAlg A st a2 = MSAlg a1 & b2 = MSAlg b1 holds
MSAlg (a1 /\ b1) = a2 /\ b2
reconsider ff1 = (*--> 0) * (signature A) as Function of (dom (signature A)),({0} *) by MSUALG_1:2;
A1: MSSign A = ManySortedSign(# {0},(dom (signature A)),ff1,((dom (signature A)) --> z) #) by MSUALG_1:10;
MSAlg (a1 /\ b1) = MSAlgebra(# (MSSorts (a1 /\ b1)),(MSCharact (a1 /\ b1)) #) by MSUALG_1:def_11;
then A2: the Sorts of (MSAlg (a1 /\ b1)) = 0 .--> the carrier of (a1 /\ b1) by MSUALG_1:def_9;
then dom the Sorts of (MSAlg (a1 /\ b1)) = the carrier of (MSSign A) by A1, FUNCOP_1:13;
then reconsider D = the Sorts of (MSAlg (a1 /\ b1)) as ManySortedSet of the carrier of (MSSign A) by PARTFUN1:def_2, RELAT_1:def_18;
let a2, b2 be strict non-empty MSSubAlgebra of MSAlg A; ::_thesis: ( a2 = MSAlg a1 & b2 = MSAlg b1 implies MSAlg (a1 /\ b1) = a2 /\ b2 )
assume A3: ( a2 = MSAlg a1 & b2 = MSAlg b1 ) ; ::_thesis: MSAlg (a1 /\ b1) = a2 /\ b2
now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_(MSSign_A)_holds_
D_._x_=_(_the_Sorts_of_a2_/\_the_Sorts_of_b2)_._x
let x be set ; ::_thesis: ( x in the carrier of (MSSign A) implies D . x = ( the Sorts of a2 /\ the Sorts of b2) . x )
A4: the carrier of a1 meets the carrier of b1 by UNIALG_2:17;
assume A5: x in the carrier of (MSSign A) ; ::_thesis: D . x = ( the Sorts of a2 /\ the Sorts of b2) . x
hence D . x = (0 .--> the carrier of (a1 /\ b1)) . 0 by A2, A1, TARSKI:def_1
.= the carrier of (a1 /\ b1) by FUNCOP_1:72
.= the carrier of a1 /\ the carrier of b1 by A4, UNIALG_2:def_9
.= (0 .--> ( the carrier of a1 /\ the carrier of b1)) . 0 by FUNCOP_1:72
.= ( the Sorts of a2 /\ the Sorts of b2) . 0 by A3, Th29
.= ( the Sorts of a2 /\ the Sorts of b2) . x by A1, A5, TARSKI:def_1 ;
::_thesis: verum
end;
then A6: D = the Sorts of a2 /\ the Sorts of b2 by PBOOLE:3;
MSSign (a1 /\ b1) = MSSign A by Th7;
then reconsider AA = MSAlg (a1 /\ b1) as strict non-empty MSSubAlgebra of MSAlg A by Th12;
for B being MSSubset of (MSAlg A) st B = the Sorts of AA holds
( B is opers_closed & the Charact of AA = Opers ((MSAlg A),B) ) by MSUALG_2:def_9;
hence MSAlg (a1 /\ b1) = a2 /\ b2 by A6, MSUALG_2:def_16; ::_thesis: verum
end;
registration
let A be quasi_total UAStr ;
cluster UAStr(# the carrier of A, the charact of A #) -> quasi_total ;
coherence
UAStr(# the carrier of A, the charact of A #) is quasi_total
proof
thus the charact of UAStr(# the carrier of A, the charact of A #) is quasi_total ; :: according to UNIALG_1:def_2 ::_thesis: verum
end;
end;
registration
let A be partial UAStr ;
cluster UAStr(# the carrier of A, the charact of A #) -> partial ;
coherence
UAStr(# the carrier of A, the charact of A #) is partial
proof
thus the charact of UAStr(# the carrier of A, the charact of A #) is homogeneous ; :: according to UNIALG_1:def_1 ::_thesis: verum
end;
end;
registration
let A be non-empty UAStr ;
cluster UAStr(# the carrier of A, the charact of A #) -> non-empty ;
coherence
UAStr(# the carrier of A, the charact of A #) is non-empty
proof
thus ( the charact of UAStr(# the carrier of A, the charact of A #) <> {} & the charact of UAStr(# the carrier of A, the charact of A #) is non-empty ) ; :: according to UNIALG_1:def_3 ::_thesis: verum
end;
end;
registration
let A be with_const_op Universal_Algebra;
cluster UAStr(# the carrier of A, the charact of A #) -> with_const_op ;
coherence
UAStr(# the carrier of A, the charact of A #) is with_const_op
proof
consider o being operation of A such that
A1: arity o = 0 by UNIALG_2:def_11;
reconsider oo = o as operation of UAStr(# the carrier of A, the charact of A #) ;
take oo ; :: according to UNIALG_2:def_11 ::_thesis: arity oo = 0
thus arity oo = 0 by A1; ::_thesis: verum
end;
end;
theorem :: MSSUBLAT:32
for A being with_const_op Universal_Algebra holds UnSubAlLattice UAStr(# the carrier of A, the charact of A #), MSSubAlLattice (MSAlg UAStr(# the carrier of A, the charact of A #)) are_isomorphic
proof
let Z be with_const_op Universal_Algebra; ::_thesis: UnSubAlLattice UAStr(# the carrier of Z, the charact of Z #), MSSubAlLattice (MSAlg UAStr(# the carrier of Z, the charact of Z #)) are_isomorphic
set A = UAStr(# the carrier of Z, the charact of Z #);
reconsider ff1 = (*--> 0) * (signature UAStr(# the carrier of Z, the charact of Z #)) as Function of (dom (signature UAStr(# the carrier of Z, the charact of Z #))),({0} *) by MSUALG_1:2;
A1: MSSign UAStr(# the carrier of Z, the charact of Z #) = ManySortedSign(# {0},(dom (signature UAStr(# the carrier of Z, the charact of Z #))),ff1,((dom (signature UAStr(# the carrier of Z, the charact of Z #))) --> z) #) by MSUALG_1:10;
defpred S1[ set , set ] means ex A1 being strict SubAlgebra of UAStr(# the carrier of Z, the charact of Z #) st
( A1 = $1 & $2 = MSAlg A1 );
A2: for x being Element of Sub UAStr(# the carrier of Z, the charact of Z #) ex y being Element of MSSub (MSAlg UAStr(# the carrier of Z, the charact of Z #)) st S1[x,y]
proof
let x be Element of Sub UAStr(# the carrier of Z, the charact of Z #); ::_thesis: ex y being Element of MSSub (MSAlg UAStr(# the carrier of Z, the charact of Z #)) st S1[x,y]
reconsider B = x as strict SubAlgebra of UAStr(# the carrier of Z, the charact of Z #) by UNIALG_2:def_14;
MSSign UAStr(# the carrier of Z, the charact of Z #) = MSSign B by Th7;
then MSAlg B is strict non-empty MSSubAlgebra of MSAlg UAStr(# the carrier of Z, the charact of Z #) by Th12;
then reconsider y = MSAlg B as Element of MSSub (MSAlg UAStr(# the carrier of Z, the charact of Z #)) by MSUALG_2:def_19;
take y ; ::_thesis: S1[x,y]
take B ; ::_thesis: ( B = x & y = MSAlg B )
thus ( B = x & y = MSAlg B ) ; ::_thesis: verum
end;
consider f being Function of (Sub UAStr(# the carrier of Z, the charact of Z #)),(MSSub (MSAlg UAStr(# the carrier of Z, the charact of Z #))) such that
A3: for x being Element of Sub UAStr(# the carrier of Z, the charact of Z #) holds S1[x,f . x] from FUNCT_2:sch_3(A2);
reconsider f = f as Function of the carrier of (UnSubAlLattice UAStr(# the carrier of Z, the charact of Z #)), the carrier of (MSSubAlLattice (MSAlg UAStr(# the carrier of Z, the charact of Z #))) ;
f is Homomorphism of UnSubAlLattice UAStr(# the carrier of Z, the charact of Z #), MSSubAlLattice (MSAlg UAStr(# the carrier of Z, the charact of Z #))
proof
let a1, b1 be Element of (UnSubAlLattice UAStr(# the carrier of Z, the charact of Z #)); :: according to LATTICE4:def_1 ::_thesis: ( f . (a1 "\/" b1) = (f . a1) "\/" (f . b1) & f . (a1 "/\" b1) = (f . a1) "/\" (f . b1) )
reconsider a2 = a1, b2 = b1 as Element of Sub UAStr(# the carrier of Z, the charact of Z #) ;
reconsider a3 = a2, b3 = b2 as strict non-empty SubAlgebra of UAStr(# the carrier of Z, the charact of Z #) by UNIALG_2:def_14;
reconsider s = a3 "\/" b3 as Element of Sub UAStr(# the carrier of Z, the charact of Z #) by UNIALG_2:def_14;
reconsider m = a3 /\ b3 as Element of Sub UAStr(# the carrier of Z, the charact of Z #) by UNIALG_2:def_14;
A4: ex A1 being strict non-empty SubAlgebra of UAStr(# the carrier of Z, the charact of Z #) st
( A1 = s & f . s = MSAlg A1 ) by A3;
MSSign b3 = MSSign UAStr(# the carrier of Z, the charact of Z #) by Th7;
then reconsider g2 = MSAlg b3 as strict non-empty MSSubAlgebra of MSAlg UAStr(# the carrier of Z, the charact of Z #) by Th12;
consider A4 being strict non-empty SubAlgebra of UAStr(# the carrier of Z, the charact of Z #) such that
A5: A4 = b3 and
A6: f . b3 = MSAlg A4 by A3;
MSSign A4 = MSSign UAStr(# the carrier of Z, the charact of Z #) by Th7;
then reconsider g3 = MSAlg A4 as strict non-empty MSSubAlgebra of MSAlg UAStr(# the carrier of Z, the charact of Z #) by Th12;
MSSign a3 = MSSign UAStr(# the carrier of Z, the charact of Z #) by Th7;
then reconsider g1 = MSAlg a3 as strict non-empty MSSubAlgebra of MSAlg UAStr(# the carrier of Z, the charact of Z #) by Th12;
consider A3 being strict non-empty SubAlgebra of UAStr(# the carrier of Z, the charact of Z #) such that
A7: A3 = a3 and
A8: f . a3 = MSAlg A3 by A3;
MSSign A3 = MSSign UAStr(# the carrier of Z, the charact of Z #) by Th7;
then reconsider g4 = MSAlg A3 as strict non-empty MSSubAlgebra of MSAlg UAStr(# the carrier of Z, the charact of Z #) by Th12;
A9: ex A1 being strict non-empty SubAlgebra of UAStr(# the carrier of Z, the charact of Z #) st
( A1 = m & f . m = MSAlg A1 ) by A3;
A10: f . (a1 "/\" b1) = f . ((UniAlg_meet UAStr(# the carrier of Z, the charact of Z #)) . (a2,b2)) by LATTICES:def_2
.= MSAlg (a3 /\ b3) by A9, UNIALG_2:def_16
.= g1 /\ g2 by Th31
.= the L_meet of (MSSubAlLattice (MSAlg UAStr(# the carrier of Z, the charact of Z #))) . ((f . a1),(f . b1)) by A7, A8, A5, A6, MSUALG_2:def_21
.= (f . a1) "/\" (f . b1) by LATTICES:def_2 ;
f . (a1 "\/" b1) = f . ((UniAlg_join UAStr(# the carrier of Z, the charact of Z #)) . (a2,b2)) by LATTICES:def_1
.= MSAlg (a3 "\/" b3) by A4, UNIALG_2:def_15
.= g4 "\/" g3 by A7, A5, Th30
.= the L_join of (MSSubAlLattice (MSAlg UAStr(# the carrier of Z, the charact of Z #))) . ((f . a1),(f . b1)) by A8, A6, MSUALG_2:def_20
.= (f . a1) "\/" (f . b1) by LATTICES:def_1 ;
hence ( f . (a1 "\/" b1) = (f . a1) "\/" (f . b1) & f . (a1 "/\" b1) = (f . a1) "/\" (f . b1) ) by A10; ::_thesis: verum
end;
then reconsider f = f as Homomorphism of UnSubAlLattice UAStr(# the carrier of Z, the charact of Z #), MSSubAlLattice (MSAlg UAStr(# the carrier of Z, the charact of Z #)) ;
take f ; :: according to LATTICE4:def_2 ::_thesis: f is bijective
now__::_thesis:_for_x1,_x2_being_set_st_x1_in_dom_f_&_x2_in_dom_f_&_f_._x1_=_f_._x2_holds_
x1_=_x2
let x1, x2 be set ; ::_thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
assume that
A11: ( x1 in dom f & x2 in dom f ) and
A12: f . x1 = f . x2 ; ::_thesis: x1 = x2
reconsider y1 = x1, y2 = x2 as Element of Sub UAStr(# the carrier of Z, the charact of Z #) by A11, FUNCT_2:def_1;
consider A1 being strict SubAlgebra of UAStr(# the carrier of Z, the charact of Z #) such that
A13: A1 = y1 and
A14: f . y1 = MSAlg A1 by A3;
consider A2 being strict SubAlgebra of UAStr(# the carrier of Z, the charact of Z #) such that
A15: ( A2 = y2 & f . y2 = MSAlg A2 ) by A3;
A16: MSSign A1 = MSSign UAStr(# the carrier of Z, the charact of Z #) by Th7
.= MSSign A2 by Th7 ;
thus x1 = 1-Alg (MSAlg A1) by A13, MSUALG_1:9
.= x2 by A12, A14, A15, A16, MSUALG_1:9 ; ::_thesis: verum
end;
hence f is one-to-one by FUNCT_1:def_4; :: according to FUNCT_2:def_4 ::_thesis: f is onto
A17: dom f = Sub UAStr(# the carrier of Z, the charact of Z #) by FUNCT_2:def_1;
thus rng f = the carrier of (MSSubAlLattice (MSAlg UAStr(# the carrier of Z, the charact of Z #))) :: according to FUNCT_2:def_3 ::_thesis: verum
proof
thus rng f c= the carrier of (MSSubAlLattice (MSAlg UAStr(# the carrier of Z, the charact of Z #))) by RELAT_1:def_19; :: according to XBOOLE_0:def_10 ::_thesis: the carrier of (MSSubAlLattice (MSAlg UAStr(# the carrier of Z, the charact of Z #))) c= rng f
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (MSSubAlLattice (MSAlg UAStr(# the carrier of Z, the charact of Z #))) or x in rng f )
assume x in the carrier of (MSSubAlLattice (MSAlg UAStr(# the carrier of Z, the charact of Z #))) ; ::_thesis: x in rng f
then reconsider y = x as strict MSSubAlgebra of MSAlg UAStr(# the carrier of Z, the charact of Z #) by MSUALG_2:def_19;
reconsider C = Constants (MSAlg UAStr(# the carrier of Z, the charact of Z #)) as MSSubset of y by MSUALG_2:10;
C c= the Sorts of y by PBOOLE:def_18;
then the Sorts of y is V2() by PBOOLE:131;
then reconsider y = y as strict non-empty MSSubAlgebra of MSAlg UAStr(# the carrier of Z, the charact of Z #) by MSUALG_1:def_3;
1-Alg y is SubAlgebra of 1-Alg (MSAlg UAStr(# the carrier of Z, the charact of Z #)) by Th20;
then 1-Alg y is SubAlgebra of UAStr(# the carrier of Z, the charact of Z #) by MSUALG_1:9;
then reconsider y1 = 1-Alg y as Element of Sub UAStr(# the carrier of Z, the charact of Z #) by UNIALG_2:def_14;
ex A1 being strict SubAlgebra of UAStr(# the carrier of Z, the charact of Z #) st
( A1 = y1 & f . y1 = MSAlg A1 ) by A3;
then A18: f . (1-Alg y) = x by A1, Th26;
y1 in dom f by A17;
hence x in rng f by A18, FUNCT_1:def_3; ::_thesis: verum
end;
end;