let S be non empty non void ManySortedSign ; :: thesis: for o being OperSymbol of S
for U1, U2, U3 being feasible MSAlgebra over S
for F being ManySortedFunction of U1,U2
for G being ManySortedFunction of U2,U3
for x being Element of Args (o,U1) st Args (o,U1) <> {} & the Sorts of U1 is_transformable_to the Sorts of U2 & the Sorts of U2 is_transformable_to the Sorts of U3 holds
ex GF being ManySortedFunction of U1,U3 st
( GF = G ** F & GF # x = G # (F # x) )
let o be OperSymbol of S; :: thesis: for U1, U2, U3 being feasible MSAlgebra over S
for F being ManySortedFunction of U1,U2
for G being ManySortedFunction of U2,U3
for x being Element of Args (o,U1) st Args (o,U1) <> {} & the Sorts of U1 is_transformable_to the Sorts of U2 & the Sorts of U2 is_transformable_to the Sorts of U3 holds
ex GF being ManySortedFunction of U1,U3 st
( GF = G ** F & GF # x = G # (F # x) )
let U1, U2, U3 be feasible MSAlgebra over S; :: thesis: for F being ManySortedFunction of U1,U2
for G being ManySortedFunction of U2,U3
for x being Element of Args (o,U1) st Args (o,U1) <> {} & the Sorts of U1 is_transformable_to the Sorts of U2 & the Sorts of U2 is_transformable_to the Sorts of U3 holds
ex GF being ManySortedFunction of U1,U3 st
( GF = G ** F & GF # x = G # (F # x) )
let F be ManySortedFunction of U1,U2; :: thesis: for G being ManySortedFunction of U2,U3
for x being Element of Args (o,U1) st Args (o,U1) <> {} & the Sorts of U1 is_transformable_to the Sorts of U2 & the Sorts of U2 is_transformable_to the Sorts of U3 holds
ex GF being ManySortedFunction of U1,U3 st
( GF = G ** F & GF # x = G # (F # x) )
let G be ManySortedFunction of U2,U3; :: thesis: for x being Element of Args (o,U1) st Args (o,U1) <> {} & the Sorts of U1 is_transformable_to the Sorts of U2 & the Sorts of U2 is_transformable_to the Sorts of U3 holds
ex GF being ManySortedFunction of U1,U3 st
( GF = G ** F & GF # x = G # (F # x) )
let x be Element of Args (o,U1); :: thesis: ( Args (o,U1) <> {} & the Sorts of U1 is_transformable_to the Sorts of U2 & the Sorts of U2 is_transformable_to the Sorts of U3 implies ex GF being ManySortedFunction of U1,U3 st
( GF = G ** F & GF # x = G # (F # x) ) )
assume that
A1: Args (o,U1) <> {} and
A2: the Sorts of U1 is_transformable_to the Sorts of U2 and
A3: the Sorts of U2 is_transformable_to the Sorts of U3 ; :: thesis: ex GF being ManySortedFunction of U1,U3 st
( GF = G ** F & GF # x = G # (F # x) )
x in Args (o,U1) by A1;
then x in product ( the Sorts of U1 * (the_arity_of o)) by PRALG_2:3;
then A4: ex g being Function st
( x = g & dom g = dom ( the Sorts of U1 * (the_arity_of o)) & ( for x being object st x in dom ( the Sorts of U1 * (the_arity_of o)) holds
g . x in ( the Sorts of U1 * (the_arity_of o)) . x ) ) by CARD_3:def 5;
then reconsider x9 = x as Function ;
reconsider Fr = (Frege (F * (the_arity_of o))) . x9 as Function ;
dom F = the carrier of S by PARTFUN1:def 2;
then A5: rng (the_arity_of o) c= dom F ;
then A6: dom (F * (the_arity_of o)) = dom (the_arity_of o) by RELAT_1:27;
A7: dom (doms (F * (the_arity_of o))) = dom (F * (the_arity_of o)) by FUNCT_6:59;
then A8: dom x9 = dom (doms (F * (the_arity_of o))) by A1, A6, MSUALG_3:6;
then reconsider x99 = x9 as ManySortedSet of dom (the_arity_of o) by A6, A7, PARTFUN1:def 2, RELAT_1:def 18;
dom G = the carrier of S by PARTFUN1:def 2;
then rng (the_arity_of o) c= dom G ;
then A9: dom (G * (the_arity_of o)) = dom (the_arity_of o) by RELAT_1:27;
then reconsider Ga = G * (the_arity_of o), Fa = F * (the_arity_of o) as ManySortedFunction of dom (the_arity_of o) by A6, PARTFUN1:def 2, RELAT_1:def 18;
A10: Args (o,U2) <> {} by A1, A2, Th3;
dom the Sorts of U1 = the carrier of S by PARTFUN1:def 2;
then A11: rng (the_arity_of o) c= dom the Sorts of U1 ;

now :: thesis: for x being object st x in dom (doms (F * (the_arity_of o))) holds
x9 . x in (doms (F * (the_arity_of o))) . x

let x be object ; :: thesis: ( x in dom (doms (F * (the_arity_of o))) implies x9 . x in (doms (F * (the_arity_of o))) . x )
set ds = (the_arity_of o) . x;
assume x in dom (doms (F * (the_arity_of o))) ; :: thesis: x9 . x in (doms (F * (the_arity_of o))) . x
then A12: x in dom (F * (the_arity_of o)) by FUNCT_6:59;
then A13: (doms (F * (the_arity_of o))) . x = dom ((F * (the_arity_of o)) . x) by FUNCT_6:22;
A14: x in dom (the_arity_of o) by A5, A12, RELAT_1:27;
then A15: (the_arity_of o) . x in rng (the_arity_of o) by FUNCT_1:def 3;
then reconsider Ff = F . ((the_arity_of o) . x) as Function of ( the Sorts of U1 . ((the_arity_of o) . x)),( the Sorts of U2 . ((the_arity_of o) . x)) by PBOOLE:def 15;
x in dom ( the Sorts of U1 * (the_arity_of o)) by A11, A14, RELAT_1:27;
then A16: x9 . x in ( the Sorts of U1 * (the_arity_of o)) . x by A1, MSUALG_3:6;
A17: the Sorts of U1 . ((the_arity_of o) . x) = dom Ff

proof

per cases ( the Sorts of U2 . ((the_arity_of o) . x) <> {} or the Sorts of U2 . ((the_arity_of o) . x) = {} ) ;

suppose the Sorts of U2 . ((the_arity_of o) . x) <> {} ; :: thesis: the Sorts of U1 . ((the_arity_of o) . x) = dom Ff

hence the Sorts of U1 . ((the_arity_of o) . x) = dom Ff by FUNCT_2:def 1; :: thesis: verum

end;

suppose the Sorts of U2 . ((the_arity_of o) . x) = {} ; :: thesis: the Sorts of U1 . ((the_arity_of o) . x) = dom Ff

then the Sorts of U1 . ((the_arity_of o) . x) = {} by A2, A15, PZFMISC1:def 3;
hence the Sorts of U1 . ((the_arity_of o) . x) = dom Ff ; :: thesis: verum

end;

end;

end;

(F * (the_arity_of o)) . x = F . ((the_arity_of o) . x) by A14, FUNCT_1:13;
hence x9 . x in (doms (F * (the_arity_of o))) . x by A13, A14, A16, A17, FUNCT_1:13; :: thesis: verum

end;

then A18: x9 in product (doms (F * (the_arity_of o))) by A8, CARD_3:9;
then A19: Fr = (F * (the_arity_of o)) .. x9 by PRALG_2:def 2;

A20: now :: thesis: for x being object st x in dom (doms (G * (the_arity_of o))) holds
Fr . x in (doms (G * (the_arity_of o))) . x

let x be object ; :: thesis: ( x in dom (doms (G * (the_arity_of o))) implies Fr . x in (doms (G * (the_arity_of o))) . x )
set ds = (the_arity_of o) . x;
assume A21: x in dom (doms (G * (the_arity_of o))) ; :: thesis: Fr . x in (doms (G * (the_arity_of o))) . x
then A22: x in dom (G * (the_arity_of o)) by FUNCT_6:59;
Z2: dom x9 = dom (the_arity_of o) by A1, MSUALG_3:6;
Z1: x in dom (F * (the_arity_of o)) by A9, A6, A21, FUNCT_6:59;
Z3: dom (F * (the_arity_of o)) = dom (the_arity_of o) by A6;
then (dom (F * (the_arity_of o))) /\ (dom x9) = dom (the_arity_of o) by Z2;
then x in (dom (F * (the_arity_of o))) /\ (dom x9) by Z1, Z3;
then x in dom ((F * (the_arity_of o)) .. x9) by PRALG_1:def 19;
then A23: Fr . x = ((F * (the_arity_of o)) . x) . (x9 . x) by A19, PRALG_1:def 19;
A24: dom ( the Sorts of U1 * (the_arity_of o)) = dom (the_arity_of o) by A11, RELAT_1:27;
A25: x in dom (the_arity_of o) by A9, A21, FUNCT_6:59;
then A26: (the_arity_of o) . x in rng (the_arity_of o) by FUNCT_1:def 3;
then reconsider Ff = F . ((the_arity_of o) . x) as Function of ( the Sorts of U1 . ((the_arity_of o) . x)),( the Sorts of U2 . ((the_arity_of o) . x)) by PBOOLE:def 15;
A27: (F * (the_arity_of o)) . x = Ff by A6, A25, FUNCT_1:12;
reconsider Gds = G . ((the_arity_of o) . x) as Function of ( the Sorts of U2 . ((the_arity_of o) . x)),( the Sorts of U3 . ((the_arity_of o) . x)) by A26, PBOOLE:def 15;
A28: dom Gds = the Sorts of U2 . ((the_arity_of o) . x)

proof

per cases ( the Sorts of U3 . ((the_arity_of o) . x) <> {} or the Sorts of U3 . ((the_arity_of o) . x) = {} ) ;

suppose the Sorts of U3 . ((the_arity_of o) . x) <> {} ; :: thesis: dom Gds = the Sorts of U2 . ((the_arity_of o) . x)

hence dom Gds = the Sorts of U2 . ((the_arity_of o) . x) by FUNCT_2:def 1; :: thesis: verum

end;

suppose the Sorts of U3 . ((the_arity_of o) . x) = {} ; :: thesis: dom Gds = the Sorts of U2 . ((the_arity_of o) . x)

then the Sorts of U2 . ((the_arity_of o) . x) = {} by A3, A26, PZFMISC1:def 3;
hence dom Gds = the Sorts of U2 . ((the_arity_of o) . x) ; :: thesis: verum

end;

end;

end;

A29: the Sorts of U1 . ((the_arity_of o) . x) = dom Ff

proof

per cases ( the Sorts of U2 . ((the_arity_of o) . x) <> {} or the Sorts of U2 . ((the_arity_of o) . x) = {} ) ;

suppose the Sorts of U2 . ((the_arity_of o) . x) <> {} ; :: thesis: the Sorts of U1 . ((the_arity_of o) . x) = dom Ff

hence the Sorts of U1 . ((the_arity_of o) . x) = dom Ff by FUNCT_2:def 1; :: thesis: verum

end;

suppose the Sorts of U2 . ((the_arity_of o) . x) = {} ; :: thesis: the Sorts of U1 . ((the_arity_of o) . x) = dom Ff

then the Sorts of U1 . ((the_arity_of o) . x) = {} by A2, A26, PZFMISC1:def 3;
hence the Sorts of U1 . ((the_arity_of o) . x) = dom Ff ; :: thesis: verum

end;

end;

end;

( the Sorts of U1 * (the_arity_of o)) . x = the Sorts of U1 . ((the_arity_of o) . x) by A25, FUNCT_1:13;
then x9 . x in dom Ff by A1, A25, A24, A29, MSUALG_3:6;
then A30: ((F * (the_arity_of o)) . x) . (x9 . x) in rng Ff by A27, FUNCT_1:def 3;
(G * (the_arity_of o)) . x = G . ((the_arity_of o) . x) by A25, FUNCT_1:13;
then Fr . x in dom ((G * (the_arity_of o)) . x) by A28, A30, A23;
hence Fr . x in (doms (G * (the_arity_of o))) . x by A22, FUNCT_6:22; :: thesis: verum

end;

reconsider GF = G ** F as ManySortedFunction of U1,U3 by A2, ALTCAT_2:4;
dom GF = the carrier of S by PARTFUN1:def 2;
then rng (the_arity_of o) c= dom GF ;
then A31: dom (GF * (the_arity_of o)) = dom (the_arity_of o) by RELAT_1:27;
A32: x99 in doms Fa

proof

let i be object ; :: according to PBOOLE:def 1 :: thesis: ( not i in dom (the_arity_of o) or x99 . i in (doms Fa) . i )
set ai = (the_arity_of o) . i;
assume A33: i in dom (the_arity_of o) ; :: thesis: x99 . i in (doms Fa) . i
then A34: (the_arity_of o) . i in rng (the_arity_of o) by FUNCT_1:def 3;
Fa . i = F . ((the_arity_of o) . i) by A33, FUNCT_1:13;
then reconsider Ew = Fa . i as Function of ( the Sorts of U1 . ((the_arity_of o) . i)),( the Sorts of U2 . ((the_arity_of o) . i)) by A34, PBOOLE:def 15;
A35: dom Ew = the Sorts of U1 . ((the_arity_of o) . i)

proof

per cases ( the Sorts of U2 . ((the_arity_of o) . i) = {} or the Sorts of U2 . ((the_arity_of o) . i) <> {} ) ;

suppose the Sorts of U2 . ((the_arity_of o) . i) = {} ; :: thesis: dom Ew = the Sorts of U1 . ((the_arity_of o) . i)

then the Sorts of U1 . ((the_arity_of o) . i) = {} by A2, A34, PZFMISC1:def 3;
hence dom Ew = the Sorts of U1 . ((the_arity_of o) . i) ; :: thesis: verum

end;

suppose the Sorts of U2 . ((the_arity_of o) . i) <> {} ; :: thesis: dom Ew = the Sorts of U1 . ((the_arity_of o) . i)

hence dom Ew = the Sorts of U1 . ((the_arity_of o) . i) by FUNCT_2:def 1; :: thesis: verum

end;

end;

end;

i in dom ( the Sorts of U1 * (the_arity_of o)) by A33, PRALG_2:3;
then x99 . i in ( the Sorts of U1 * (the_arity_of o)) . i by A4;
then x99 . i in dom (Fa . i) by A33, A35, FUNCT_1:13;
hence x99 . i in (doms Fa) . i by A33, MSSUBFAM:14; :: thesis: verum

end;

take GF ; :: thesis: ( GF = G ** F & GF # x = G # (F # x) )
thus GF = G ** F ; :: thesis: GF # x = G # (F # x)
A36: (G * (the_arity_of o)) ** (F * (the_arity_of o)) = GF * (the_arity_of o) by FUNCTOR0:12;
A37: the Sorts of U1 is_transformable_to the Sorts of U3 by A2, A3, AUTALG_1:10;
set tao = the_arity_of o;

A38: now :: thesis: for x being object st x in dom (doms (GF * (the_arity_of o))) holds
x9 . x in (doms (GF * (the_arity_of o))) . x

let x be object ; :: thesis: ( x in dom (doms (GF * (the_arity_of o))) implies x9 . x in (doms (GF * (the_arity_of o))) . x )
set ds = (the_arity_of o) . x;
assume A39: x in dom (doms (GF * (the_arity_of o))) ; :: thesis: x9 . x in (doms (GF * (the_arity_of o))) . x
then A40: x in dom (the_arity_of o) by A31, FUNCT_6:59;
then A41: (the_arity_of o) . x in rng (the_arity_of o) by FUNCT_1:def 3;
then reconsider Gf = GF . ((the_arity_of o) . x) as Function of ( the Sorts of U1 . ((the_arity_of o) . x)),( the Sorts of U3 . ((the_arity_of o) . x)) by PBOOLE:def 15;
x in dom (GF * (the_arity_of o)) by A39, FUNCT_6:59;
then A42: (doms (GF * (the_arity_of o))) . x = dom ((GF * (the_arity_of o)) . x) by FUNCT_6:22;
A43: the Sorts of U1 . ((the_arity_of o) . x) = dom Gf

proof

per cases ( the Sorts of U3 . ((the_arity_of o) . x) <> {} or the Sorts of U3 . ((the_arity_of o) . x) = {} ) ;

suppose the Sorts of U3 . ((the_arity_of o) . x) <> {} ; :: thesis: the Sorts of U1 . ((the_arity_of o) . x) = dom Gf

hence the Sorts of U1 . ((the_arity_of o) . x) = dom Gf by FUNCT_2:def 1; :: thesis: verum

end;

suppose the Sorts of U3 . ((the_arity_of o) . x) = {} ; :: thesis: the Sorts of U1 . ((the_arity_of o) . x) = dom Gf

then the Sorts of U1 . ((the_arity_of o) . x) = {} by A37, A41, PZFMISC1:def 3;
hence the Sorts of U1 . ((the_arity_of o) . x) = dom Gf ; :: thesis: verum

end;

end;

end;

x in dom ( the Sorts of U1 * (the_arity_of o)) by A11, A40, RELAT_1:27;
then x9 . x in ( the Sorts of U1 * (the_arity_of o)) . x by A1, MSUALG_3:6;
then x9 . x in dom (GF . ((the_arity_of o) . x)) by A40, A43, FUNCT_1:13;
hence x9 . x in (doms (GF * (the_arity_of o))) . x by A42, A40, FUNCT_1:13; :: thesis: verum

end;

dom (doms (GF * (the_arity_of o))) = dom (GF * (the_arity_of o)) by FUNCT_6:59;
then dom x9 = dom (doms (GF * (the_arity_of o))) by A1, A31, MSUALG_3:6;
then A44: x9 in product (doms (GF * (the_arity_of o))) by A38, CARD_3:9;
rng (the_arity_of o) c= dom F by A5;
then S2: dom (F * (the_arity_of o)) = dom (the_arity_of o) by RELAT_1:27;
S0: dom (the_arity_of o) = dom x99 by A1, MSUALG_3:6;
dom Fr = (dom (F * (the_arity_of o))) /\ (dom x99) by A19, PRALG_1:def 19
.= dom (G * (the_arity_of o)) by A9, S0, S2 ;
then dom Fr = dom (doms (G * (the_arity_of o))) by FUNCT_6:59;
then Fr in product (doms (G * (the_arity_of o))) by A20, CARD_3:9;
then A45: (Frege (G * (the_arity_of o))) . ((Frege (F * (the_arity_of o))) . x) = (G * (the_arity_of o)) .. ((Frege (F * (the_arity_of o))) . x) by PRALG_2:def 2
.= Ga .. (Fa .. x99) by A18, PRALG_2:def 2
.= (Ga ** Fa) .. x99 by A32, CLOSURE1:4 ;
A46: Args (o,U3) <> {} by A1, A2, A3, Th3, AUTALG_1:10;
then GF # x = (Frege (GF * (the_arity_of o))) . x by A1, MSUALG_3:def 5
.= (Frege (G * (the_arity_of o))) . ((Frege (F * (the_arity_of o))) . x) by A44, A45, A36, PRALG_2:def 2
.= (Frege (G * (the_arity_of o))) . (F # x) by A1, A10, MSUALG_3:def 5 ;
hence GF # x = G # (F # x) by A10, A46, MSUALG_3:def 5; :: thesis: verum