set u2 = F .:.: the Sorts of U1;
A2: now :: thesis: for i being object st i in the carrier of S holds
not (F .:.: the Sorts of U1) . i is empty
let i be object ; :: thesis: ( i in the carrier of S implies not (F .:.: the Sorts of U1) . i is empty )
reconsider f = F . i as Function ;
assume A3: i in the carrier of S ; :: thesis: not (F .:.: the Sorts of U1) . i is empty
then A4: (F .:.: the Sorts of U1) . i = f .: ( the Sorts of U1 . i) by PBOOLE:def 20;
reconsider f = f as Function of ( the Sorts of U1 . i),( the Sorts of U2 . i) by ;
dom f = the Sorts of U1 . i by ;
hence not (F .:.: the Sorts of U1) . i is empty by A3, A4; :: thesis: verum
end;
now :: thesis: for i being object st i in the carrier of S holds
(F .:.: the Sorts of U1) . i c= the Sorts of U2 . i
let i be object ; :: thesis: ( i in the carrier of S implies (F .:.: the Sorts of U1) . i c= the Sorts of U2 . i )
reconsider f = F . i as Function ;
assume A5: i in the carrier of S ; :: thesis: (F .:.: the Sorts of U1) . i c= the Sorts of U2 . i
then A6: (F .:.: the Sorts of U1) . i = f .: ( the Sorts of U1 . i) by PBOOLE:def 20;
reconsider f = f as Function of ( the Sorts of U1 . i),( the Sorts of U2 . i) by ;
A7: rng f c= the Sorts of U2 . i by RELAT_1:def 19;
dom f = the Sorts of U1 . i by ;
hence (F .:.: the Sorts of U1) . i c= the Sorts of U2 . i by ; :: thesis: verum
end;
then F .:.: the Sorts of U1 c= the Sorts of U2 by PBOOLE:def 2;
then reconsider u2 = F .:.: the Sorts of U1 as V2() MSSubset of U2 by ;
set M = GenMSAlg u2;
reconsider M9 = MSAlgebra(# u2,(Opers (U2,u2)) #) as non-empty MSAlgebra over S by MSUALG_1:def 3;
take GenMSAlg u2 ; :: thesis: the Sorts of (GenMSAlg u2) = F .:.: the Sorts of U1
u2 is opers_closed
proof
let o be OperSymbol of S; :: according to MSUALG_2:def 6 :: thesis: u2 is_closed_on o
thus rng ((Den (o,U2)) | (((u2 #) * the Arity of S) . o)) c= (u2 * the ResultSort of S) . o :: according to MSUALG_2:def 5 :: thesis: verum
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng ((Den (o,U2)) | (((u2 #) * the Arity of S) . o)) or x in (u2 * the ResultSort of S) . o )
set D = Den (o,U2);
set X = ((u2 #) * the Arity of S) . o;
set ao = the_arity_of o;
set ro = the_result_sort_of o;
set ut = u2 * ();
set S1 = the Sorts of U1;
A8: rng () c= the carrier of S by FINSEQ_1:def 4;
A9: dom the Arity of S = the carrier' of S by FUNCT_2:def 1;
then dom ((u2 #) * the Arity of S) = dom the Arity of S by PARTFUN1:def 2;
then A10: ((u2 #) * the Arity of S) . o = (u2 #) . ( the Arity of S . o) by
.= (u2 #) . () by MSUALG_1:def 1
.= product (u2 * ()) by FINSEQ_2:def 5 ;
assume x in rng ((Den (o,U2)) | (((u2 #) * the Arity of S) . o)) ; :: thesis: x in (u2 * the ResultSort of S) . o
then consider a being object such that
A11: a in dom ((Den (o,U2)) | (((u2 #) * the Arity of S) . o)) and
A12: x = ((Den (o,U2)) | (((u2 #) * the Arity of S) . o)) . a by FUNCT_1:def 3;
A13: x = (Den (o,U2)) . a by ;
dom ((Den (o,U2)) | (((u2 #) * the Arity of S) . o)) c= dom (Den (o,U2)) by RELAT_1:60;
then reconsider a = a as Element of Args (o,U2) by ;
defpred S1[ object , object ] means for s being SortSymbol of S st s = () . \$1 holds
( \$2 in the Sorts of U1 . s & a . \$1 = (F . s) . \$2 );
A14: dom ((Den (o,U2)) | (((u2 #) * the Arity of S) . o)) c= ((u2 #) * the Arity of S) . o by RELAT_1:58;
then A15: dom a = dom (u2 * ()) by ;
A16: dom u2 = the carrier of S by PARTFUN1:def 2;
A17: for y being object st y in dom a holds
ex i being object st S1[y,i]
proof
let y be object ; :: thesis: ( y in dom a implies ex i being object st S1[y,i] )
assume A18: y in dom a ; :: thesis: ex i being object st S1[y,i]
then A19: a . y in (u2 * ()) . y by ;
dom (u2 * ()) = dom () by ;
then (the_arity_of o) . y in rng () by ;
then reconsider s = () . y as SortSymbol of S by A8;
A20: dom (F . s) = the Sorts of U1 . s by FUNCT_2:def 1;
(u2 * ()) . y = u2 . (() . y) by
.= (F . s) .: ( the Sorts of U1 . s) by PBOOLE:def 20
.= rng (F . s) by ;
then consider i being object such that
A21: ( i in the Sorts of U1 . s & a . y = (F . s) . i ) by ;
take i ; :: thesis: S1[y,i]
thus S1[y,i] by A21; :: thesis: verum
end;
consider f being Function such that
A22: ( dom f = dom a & ( for y being object st y in dom a holds
S1[y,f . y] ) ) from dom the Sorts of U1 = the carrier of S by PARTFUN1:def 2;
then A23: dom ( the Sorts of U1 * ()) = dom () by ;
A24: dom f = dom () by ;
A25: for y being object st y in dom ( the Sorts of U1 * ()) holds
f . y in ( the Sorts of U1 * ()) . y
proof
let y be object ; :: thesis: ( y in dom ( the Sorts of U1 * ()) implies f . y in ( the Sorts of U1 * ()) . y )
assume A26: y in dom ( the Sorts of U1 * ()) ; :: thesis: f . y in ( the Sorts of U1 * ()) . y
then (the_arity_of o) . y in rng () by ;
then reconsider s = () . y as SortSymbol of S by A8;
f . y in the Sorts of U1 . s by A22, A24, A23, A26;
hence f . y in ( the Sorts of U1 * ()) . y by ; :: thesis: verum
end;
Args (o,U1) = product ( the Sorts of U1 * ()) by PRALG_2:3;
then reconsider a1 = f as Element of Args (o,U1) by ;
A27: dom a1 = dom () by Th6;
A28: now :: thesis: for y being object st y in dom () holds
(F # a1) . y = a . y
let y be object ; :: thesis: ( y in dom () implies (F # a1) . y = a . y )
assume A29: y in dom () ; :: thesis: (F # a1) . y = a . y
then reconsider n = y as Nat ;
(the_arity_of o) . y in rng () by ;
then reconsider s = () . y as SortSymbol of S by A8;
(F # a1) . n = (F . (() /. n)) . (a1 . n) by
.= (F . s) . (a1 . n) by ;
hence (F # a1) . y = a . y by ; :: thesis: verum
end;
( dom (F # a1) = dom () & dom a = dom () ) by Th6;
then F # a1 = a by ;
then A30: (F . ) . ((Den (o,U1)) . a1) = x by ;
reconsider g = F . as Function ;
A31: dom (F . ) = the Sorts of U1 . by FUNCT_2:def 1;
A32: dom the ResultSort of S = the carrier' of S by FUNCT_2:def 1;
then A33: dom ( the Sorts of U1 * the ResultSort of S) = dom the ResultSort of S by PARTFUN1:def 2;
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
.= the Sorts of U1 . by MSUALG_1:def 2 ;
then (Den (o,U1)) . a1 in the Sorts of U1 . ;
then A34: (Den (o,U1)) . a1 in dom (F . ) by FUNCT_2:def 1;
dom (u2 * the ResultSort of S) = dom the ResultSort of S by ;
then (u2 * the ResultSort of S) . o = u2 . ( the ResultSort of S . o) by
.= u2 . by MSUALG_1:def 2
.= g .: ( the Sorts of U1 . ) by PBOOLE:def 20
.= rng g by ;
hence x in (u2 * the ResultSort of S) . o by ; :: thesis: verum
end;
end;
then for B being MSSubset of U2 st B = the Sorts of M9 holds
( B is opers_closed & the Charact of M9 = Opers (U2,B) ) ;
then A35: M9 is MSSubAlgebra of U2 by MSUALG_2:def 9;
u2 is MSSubset of M9 by PBOOLE:def 18;
then GenMSAlg u2 is MSSubAlgebra of M9 by ;
then the Sorts of (GenMSAlg u2) is MSSubset of M9 by MSUALG_2:def 9;
then A36: the Sorts of (GenMSAlg u2) c= u2 by PBOOLE:def 18;
u2 is MSSubset of (GenMSAlg u2) by MSUALG_2:def 17;
then u2 c= the Sorts of (GenMSAlg u2) by PBOOLE:def 18;
hence the Sorts of (GenMSAlg u2) = F .:.: the Sorts of U1 by ; :: thesis: verum