set u2 = F .:.: the Sorts of U1;

then reconsider u2 = F .:.: the Sorts of U1 as V2() MSSubset of U2 by A2, PBOOLE:def 13, PBOOLE:def 18;

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

( 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 A35, MSUALG_2:def 17;

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 A36, PBOOLE:146; :: thesis: verum

A2: now :: thesis: for i being object st i in the carrier of S holds

not (F .:.: the Sorts of U1) . i is empty

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 A3, PBOOLE:def 15;

dom f = the Sorts of U1 . i by A3, FUNCT_2:def 1;

hence not (F .:.: the Sorts of U1) . i is empty by A3, A4; :: thesis: verum

end;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 A3, PBOOLE:def 15;

dom f = the Sorts of U1 . i by A3, FUNCT_2:def 1;

hence not (F .:.: the Sorts of U1) . i is empty by A3, A4; :: thesis: verum

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

then
F .:.: the Sorts of U1 c= the Sorts of U2
by PBOOLE:def 2;(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 A5, PBOOLE:def 15;

A7: rng f c= the Sorts of U2 . i by RELAT_1:def 19;

dom f = the Sorts of U1 . i by A5, FUNCT_2:def 1;

hence (F .:.: the Sorts of U1) . i c= the Sorts of U2 . i by A6, A7, RELAT_1:113; :: thesis: verum

end;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 A5, PBOOLE:def 15;

A7: rng f c= the Sorts of U2 . i by RELAT_1:def 19;

dom f = the Sorts of U1 . i by A5, FUNCT_2:def 1;

hence (F .:.: the Sorts of U1) . i c= the Sorts of U2 . i by A6, A7, RELAT_1:113; :: thesis: verum

then reconsider u2 = F .:.: the Sorts of U1 as V2() MSSubset of U2 by A2, PBOOLE:def 13, PBOOLE:def 18;

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

then
for B being MSSubset of U2 st B = the Sorts of M9 holds
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

end;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 * (the_arity_of o);

set S1 = the Sorts of U1;

A8: rng (the_arity_of o) 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 A9, FUNCT_1:12

.= (u2 #) . (the_arity_of o) by MSUALG_1:def 1

.= product (u2 * (the_arity_of o)) 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 A11, A12, FUNCT_1:47;

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 A11, FUNCT_2:def 1;

defpred S_{1}[ object , object ] means for s being SortSymbol of S st s = (the_arity_of o) . $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 * (the_arity_of o)) by A11, A10, CARD_3:9;

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 S_{1}[y,i]

A22: ( dom f = dom a & ( for y being object st y in dom a holds

S_{1}[y,f . y] ) )
from CLASSES1:sch 1(A17);

dom the Sorts of U1 = the carrier of S by PARTFUN1:def 2;

then A23: dom ( the Sorts of U1 * (the_arity_of o)) = dom (the_arity_of o) by A8, RELAT_1:27;

A24: dom f = dom (the_arity_of o) by A15, A16, A8, A22, RELAT_1:27;

A25: for y being object st y in dom ( the Sorts of U1 * (the_arity_of o)) holds

f . y in ( the Sorts of U1 * (the_arity_of o)) . y

then reconsider a1 = f as Element of Args (o,U1) by A24, A23, A25, CARD_3:9;

A27: dom a1 = dom (the_arity_of o) by Th6;

then F # a1 = a by A28, FUNCT_1:2;

then A30: (F . (the_result_sort_of o)) . ((Den (o,U1)) . a1) = x by A1, A13;

reconsider g = F . (the_result_sort_of o) as Function ;

A31: dom (F . (the_result_sort_of o)) = the Sorts of U1 . (the_result_sort_of o) 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 A32, A33, FUNCT_1:12

.= the Sorts of U1 . (the_result_sort_of o) by MSUALG_1:def 2 ;

then (Den (o,U1)) . a1 in the Sorts of U1 . (the_result_sort_of o) ;

then A34: (Den (o,U1)) . a1 in dom (F . (the_result_sort_of o)) by FUNCT_2:def 1;

dom (u2 * the ResultSort of S) = dom the ResultSort of S by A32, PARTFUN1:def 2;

then (u2 * the ResultSort of S) . o = u2 . ( the ResultSort of S . o) by A32, FUNCT_1:12

.= u2 . (the_result_sort_of o) by MSUALG_1:def 2

.= g .: ( the Sorts of U1 . (the_result_sort_of o)) by PBOOLE:def 20

.= rng g by A31, RELAT_1:113 ;

hence x in (u2 * the ResultSort of S) . o by A30, A34, FUNCT_1:def 3; :: thesis: verum

end;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 * (the_arity_of o);

set S1 = the Sorts of U1;

A8: rng (the_arity_of o) 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 A9, FUNCT_1:12

.= (u2 #) . (the_arity_of o) by MSUALG_1:def 1

.= product (u2 * (the_arity_of o)) 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 A11, A12, FUNCT_1:47;

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 A11, FUNCT_2:def 1;

defpred S

( $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 * (the_arity_of o)) by A11, A10, CARD_3:9;

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 S

proof

consider f being Function such that
let y be object ; :: thesis: ( y in dom a implies ex i being object st S_{1}[y,i] )

assume A18: y in dom a ; :: thesis: ex i being object st S_{1}[y,i]

then A19: a . y in (u2 * (the_arity_of o)) . y by A11, A14, A10, A15, CARD_3:9;

dom (u2 * (the_arity_of o)) = dom (the_arity_of o) by A16, A8, RELAT_1:27;

then (the_arity_of o) . y in rng (the_arity_of o) by A15, A18, FUNCT_1:def 3;

then reconsider s = (the_arity_of o) . y as SortSymbol of S by A8;

A20: dom (F . s) = the Sorts of U1 . s by FUNCT_2:def 1;

(u2 * (the_arity_of o)) . y = u2 . ((the_arity_of o) . y) by A15, A18, FUNCT_1:12

.= (F . s) .: ( the Sorts of U1 . s) by PBOOLE:def 20

.= rng (F . s) by A20, RELAT_1:113 ;

then consider i being object such that

A21: ( i in the Sorts of U1 . s & a . y = (F . s) . i ) by A20, A19, FUNCT_1:def 3;

take i ; :: thesis: S_{1}[y,i]

thus S_{1}[y,i]
by A21; :: thesis: verum

end;assume A18: y in dom a ; :: thesis: ex i being object st S

then A19: a . y in (u2 * (the_arity_of o)) . y by A11, A14, A10, A15, CARD_3:9;

dom (u2 * (the_arity_of o)) = dom (the_arity_of o) by A16, A8, RELAT_1:27;

then (the_arity_of o) . y in rng (the_arity_of o) by A15, A18, FUNCT_1:def 3;

then reconsider s = (the_arity_of o) . y as SortSymbol of S by A8;

A20: dom (F . s) = the Sorts of U1 . s by FUNCT_2:def 1;

(u2 * (the_arity_of o)) . y = u2 . ((the_arity_of o) . y) by A15, A18, FUNCT_1:12

.= (F . s) .: ( the Sorts of U1 . s) by PBOOLE:def 20

.= rng (F . s) by A20, RELAT_1:113 ;

then consider i being object such that

A21: ( i in the Sorts of U1 . s & a . y = (F . s) . i ) by A20, A19, FUNCT_1:def 3;

take i ; :: thesis: S

thus S

A22: ( dom f = dom a & ( for y being object st y in dom a holds

S

dom the Sorts of U1 = the carrier of S by PARTFUN1:def 2;

then A23: dom ( the Sorts of U1 * (the_arity_of o)) = dom (the_arity_of o) by A8, RELAT_1:27;

A24: dom f = dom (the_arity_of o) by A15, A16, A8, A22, RELAT_1:27;

A25: for y being object st y in dom ( the Sorts of U1 * (the_arity_of o)) holds

f . y in ( the Sorts of U1 * (the_arity_of o)) . y

proof

Args (o,U1) = product ( the Sorts of U1 * (the_arity_of o))
by PRALG_2:3;
let y be object ; :: thesis: ( y in dom ( the Sorts of U1 * (the_arity_of o)) implies f . y in ( the Sorts of U1 * (the_arity_of o)) . y )

assume A26: y in dom ( the Sorts of U1 * (the_arity_of o)) ; :: thesis: f . y in ( the Sorts of U1 * (the_arity_of o)) . y

then (the_arity_of o) . y in rng (the_arity_of o) by A23, FUNCT_1:def 3;

then reconsider s = (the_arity_of o) . 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 * (the_arity_of o)) . y by A26, FUNCT_1:12; :: thesis: verum

end;assume A26: y in dom ( the Sorts of U1 * (the_arity_of o)) ; :: thesis: f . y in ( the Sorts of U1 * (the_arity_of o)) . y

then (the_arity_of o) . y in rng (the_arity_of o) by A23, FUNCT_1:def 3;

then reconsider s = (the_arity_of o) . 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 * (the_arity_of o)) . y by A26, FUNCT_1:12; :: thesis: verum

then reconsider a1 = f as Element of Args (o,U1) by A24, A23, A25, CARD_3:9;

A27: dom a1 = dom (the_arity_of o) by Th6;

A28: now :: thesis: for y being object st y in dom (the_arity_of o) holds

(F # a1) . y = a . y

( dom (F # a1) = dom (the_arity_of o) & dom a = dom (the_arity_of o) )
by Th6;(F # a1) . y = a . y

let y be object ; :: thesis: ( y in dom (the_arity_of o) implies (F # a1) . y = a . y )

assume A29: y in dom (the_arity_of o) ; :: thesis: (F # a1) . y = a . y

then reconsider n = y as Nat ;

(the_arity_of o) . y in rng (the_arity_of o) by A29, FUNCT_1:def 3;

then reconsider s = (the_arity_of o) . y as SortSymbol of S by A8;

(F # a1) . n = (F . ((the_arity_of o) /. n)) . (a1 . n) by A27, A29, Def6

.= (F . s) . (a1 . n) by A29, PARTFUN1:def 6 ;

hence (F # a1) . y = a . y by A22, A27, A29; :: thesis: verum

end;assume A29: y in dom (the_arity_of o) ; :: thesis: (F # a1) . y = a . y

then reconsider n = y as Nat ;

(the_arity_of o) . y in rng (the_arity_of o) by A29, FUNCT_1:def 3;

then reconsider s = (the_arity_of o) . y as SortSymbol of S by A8;

(F # a1) . n = (F . ((the_arity_of o) /. n)) . (a1 . n) by A27, A29, Def6

.= (F . s) . (a1 . n) by A29, PARTFUN1:def 6 ;

hence (F # a1) . y = a . y by A22, A27, A29; :: thesis: verum

then F # a1 = a by A28, FUNCT_1:2;

then A30: (F . (the_result_sort_of o)) . ((Den (o,U1)) . a1) = x by A1, A13;

reconsider g = F . (the_result_sort_of o) as Function ;

A31: dom (F . (the_result_sort_of o)) = the Sorts of U1 . (the_result_sort_of o) 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 A32, A33, FUNCT_1:12

.= the Sorts of U1 . (the_result_sort_of o) by MSUALG_1:def 2 ;

then (Den (o,U1)) . a1 in the Sorts of U1 . (the_result_sort_of o) ;

then A34: (Den (o,U1)) . a1 in dom (F . (the_result_sort_of o)) by FUNCT_2:def 1;

dom (u2 * the ResultSort of S) = dom the ResultSort of S by A32, PARTFUN1:def 2;

then (u2 * the ResultSort of S) . o = u2 . ( the ResultSort of S . o) by A32, FUNCT_1:12

.= u2 . (the_result_sort_of o) by MSUALG_1:def 2

.= g .: ( the Sorts of U1 . (the_result_sort_of o)) by PBOOLE:def 20

.= rng g by A31, RELAT_1:113 ;

hence x in (u2 * the ResultSort of S) . o by A30, A34, FUNCT_1:def 3; :: thesis: verum

( 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 A35, MSUALG_2:def 17;

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 A36, PBOOLE:146; :: thesis: verum