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 * ()) by PRALG_2:3;
then A4: ex g being Function st
( x = g & dom g = dom ( the Sorts of U1 * ()) & ( for x being object st x in dom ( the Sorts of U1 * ()) holds
g . x in ( the Sorts of U1 * ()) . x ) ) by CARD_3:def 5;
then reconsider x9 = x as Function ;
reconsider Fr = (Frege (F * ())) . x9 as Function ;
dom F = the carrier of S by PARTFUN1:def 2;
then A5: rng () c= dom F ;
then A6: dom (F * ()) = dom () by RELAT_1:27;
A7: dom (doms (F * ())) = dom (F * ()) by FUNCT_6:59;
then A8: dom x9 = dom (doms (F * ())) by ;
then reconsider x99 = x9 as ManySortedSet of dom () by ;
dom G = the carrier of S by PARTFUN1:def 2;
then rng () c= dom G ;
then A9: dom (G * ()) = dom () by RELAT_1:27;
then reconsider Ga = G * (), Fa = F * () as ManySortedFunction of dom () by ;
A10: Args (o,U2) <> {} by A1, A2, Th3;
dom the Sorts of U1 = the carrier of S by PARTFUN1:def 2;
then A11: rng () c= dom the Sorts of U1 ;
now :: thesis: for x being object st x in dom (doms (F * ())) holds
x9 . x in (doms (F * ())) . x
let x be object ; :: thesis: ( x in dom (doms (F * ())) implies x9 . x in (doms (F * ())) . x )
set ds = () . x;
assume x in dom (doms (F * ())) ; :: thesis: x9 . x in (doms (F * ())) . x
then A12: x in dom (F * ()) by FUNCT_6:59;
then A13: (doms (F * ())) . x = dom ((F * ()) . x) by FUNCT_6:22;
A14: x in dom () by ;
then A15: (the_arity_of o) . x in rng () by FUNCT_1:def 3;
then reconsider Ff = F . (() . x) as Function of ( the Sorts of U1 . (() . x)),( the Sorts of U2 . (() . x)) by PBOOLE:def 15;
x in dom ( the Sorts of U1 * ()) by ;
then A16: x9 . x in ( the Sorts of U1 * ()) . x by ;
A17: the Sorts of U1 . (() . x) = dom Ff
proof
per cases ( the Sorts of U2 . (() . x) <> {} or the Sorts of U2 . (() . x) = {} ) ;
suppose the Sorts of U2 . (() . x) <> {} ; :: thesis: the Sorts of U1 . (() . x) = dom Ff
hence the Sorts of U1 . (() . x) = dom Ff by FUNCT_2:def 1; :: thesis: verum
end;
suppose the Sorts of U2 . (() . x) = {} ; :: thesis: the Sorts of U1 . (() . x) = dom Ff
then the Sorts of U1 . (() . x) = {} by ;
hence the Sorts of U1 . (() . x) = dom Ff ; :: thesis: verum
end;
end;
end;
(F * ()) . x = F . (() . x) by ;
hence x9 . x in (doms (F * ())) . x by ; :: thesis: verum
end;
then A18: x9 in product (doms (F * ())) by ;
then A19: Fr = (F * ()) .. x9 by PRALG_2:def 2;
A20: now :: thesis: for x being object st x in dom (doms (G * ())) holds
Fr . x in (doms (G * ())) . x
let x be object ; :: thesis: ( x in dom (doms (G * ())) implies Fr . x in (doms (G * ())) . x )
set ds = () . x;
assume A21: x in dom (doms (G * ())) ; :: thesis: Fr . x in (doms (G * ())) . x
then A22: x in dom (G * ()) by FUNCT_6:59;
Z2: dom x9 = dom () by ;
Z1: x in dom (F * ()) by ;
Z3: dom (F * ()) = dom () by A6;
then Z4: (dom (F * ())) /\ (dom x9) = dom () by Z2;
then x in (dom (F * ())) /\ (dom x9) by Z1, Z3;
then x in dom ((F * ()) .. x9) by PRALG_1:def 19;
then A23: Fr . x = ((F * ()) . x) . (x9 . x) by ;
A24: dom ( the Sorts of U1 * ()) = dom () by ;
A25: x in dom () by ;
then A26: (the_arity_of o) . x in rng () by FUNCT_1:def 3;
then reconsider Ff = F . (() . x) as Function of ( the Sorts of U1 . (() . x)),( the Sorts of U2 . (() . x)) by PBOOLE:def 15;
A27: (F * ()) . x = Ff by ;
reconsider Gds = G . (() . x) as Function of ( the Sorts of U2 . (() . x)),( the Sorts of U3 . (() . x)) by ;
A28: dom Gds = the Sorts of U2 . (() . x)
proof
per cases ( the Sorts of U3 . (() . x) <> {} or the Sorts of U3 . (() . x) = {} ) ;
suppose the Sorts of U3 . (() . x) <> {} ; :: thesis: dom Gds = the Sorts of U2 . (() . x)
hence dom Gds = the Sorts of U2 . (() . x) by FUNCT_2:def 1; :: thesis: verum
end;
suppose the Sorts of U3 . (() . x) = {} ; :: thesis: dom Gds = the Sorts of U2 . (() . x)
then the Sorts of U2 . (() . x) = {} by ;
hence dom Gds = the Sorts of U2 . (() . x) ; :: thesis: verum
end;
end;
end;
A29: the Sorts of U1 . (() . x) = dom Ff
proof
per cases ( the Sorts of U2 . (() . x) <> {} or the Sorts of U2 . (() . x) = {} ) ;
suppose the Sorts of U2 . (() . x) <> {} ; :: thesis: the Sorts of U1 . (() . x) = dom Ff
hence the Sorts of U1 . (() . x) = dom Ff by FUNCT_2:def 1; :: thesis: verum
end;
suppose the Sorts of U2 . (() . x) = {} ; :: thesis: the Sorts of U1 . (() . x) = dom Ff
then the Sorts of U1 . (() . x) = {} by ;
hence the Sorts of U1 . (() . x) = dom Ff ; :: thesis: verum
end;
end;
end;
( the Sorts of U1 * ()) . x = the Sorts of U1 . (() . x) by ;
then x9 . x in dom Ff by ;
then A30: ((F * ()) . x) . (x9 . x) in rng Ff by ;
(G * ()) . x = G . (() . x) by ;
then Fr . x in dom ((G * ()) . x) by ;
hence Fr . x in (doms (G * ())) . x by ; :: thesis: verum
end;
reconsider GF = G ** F as ManySortedFunction of U1,U3 by ;
dom GF = the carrier of S by PARTFUN1:def 2;
then rng () c= dom GF ;
then A31: dom (GF * ()) = dom () by RELAT_1:27;
A32: x99 in doms Fa
proof
let i be object ; :: according to PBOOLE:def 1 :: thesis: ( not i in dom () or x99 . i in (doms Fa) . i )
set ai = () . i;
assume A33: i in dom () ; :: thesis: x99 . i in (doms Fa) . i
then A34: (the_arity_of o) . i in rng () by FUNCT_1:def 3;
Fa . i = F . (() . i) by ;
then reconsider Ew = Fa . i as Function of ( the Sorts of U1 . (() . i)),( the Sorts of U2 . (() . i)) by ;
A35: dom Ew = the Sorts of U1 . (() . i)
proof
per cases ( the Sorts of U2 . (() . i) = {} or the Sorts of U2 . (() . i) <> {} ) ;
suppose the Sorts of U2 . (() . i) = {} ; :: thesis: dom Ew = the Sorts of U1 . (() . i)
then the Sorts of U1 . (() . i) = {} by ;
hence dom Ew = the Sorts of U1 . (() . i) ; :: thesis: verum
end;
suppose the Sorts of U2 . (() . i) <> {} ; :: thesis: dom Ew = the Sorts of U1 . (() . i)
hence dom Ew = the Sorts of U1 . (() . i) by FUNCT_2:def 1; :: thesis: verum
end;
end;
end;
i in dom ( the Sorts of U1 * ()) by ;
then x99 . i in ( the Sorts of U1 * ()) . i by A4;
then x99 . i in dom (Fa . i) by ;
hence x99 . i in (doms Fa) . i by ; :: 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 * ()) ** (F * ()) = GF * () by FUNCTOR0:12;
A37: the Sorts of U1 is_transformable_to the Sorts of U3 by ;
set tao = the_arity_of o;
A38: now :: thesis: for x being object st x in dom (doms (GF * ())) holds
x9 . x in (doms (GF * ())) . x
let x be object ; :: thesis: ( x in dom (doms (GF * ())) implies x9 . x in (doms (GF * ())) . x )
set ds = () . x;
assume A39: x in dom (doms (GF * ())) ; :: thesis: x9 . x in (doms (GF * ())) . x
then A40: x in dom () by ;
then A41: (the_arity_of o) . x in rng () by FUNCT_1:def 3;
then reconsider Gf = GF . (() . x) as Function of ( the Sorts of U1 . (() . x)),( the Sorts of U3 . (() . x)) by PBOOLE:def 15;
x in dom (GF * ()) by ;
then A42: (doms (GF * ())) . x = dom ((GF * ()) . x) by FUNCT_6:22;
A43: the Sorts of U1 . (() . x) = dom Gf
proof
per cases ( the Sorts of U3 . (() . x) <> {} or the Sorts of U3 . (() . x) = {} ) ;
suppose the Sorts of U3 . (() . x) <> {} ; :: thesis: the Sorts of U1 . (() . x) = dom Gf
hence the Sorts of U1 . (() . x) = dom Gf by FUNCT_2:def 1; :: thesis: verum
end;
suppose the Sorts of U3 . (() . x) = {} ; :: thesis: the Sorts of U1 . (() . x) = dom Gf
then the Sorts of U1 . (() . x) = {} by ;
hence the Sorts of U1 . (() . x) = dom Gf ; :: thesis: verum
end;
end;
end;
x in dom ( the Sorts of U1 * ()) by ;
then x9 . x in ( the Sorts of U1 * ()) . x by ;
then x9 . x in dom (GF . (() . x)) by ;
hence x9 . x in (doms (GF * ())) . x by ; :: thesis: verum
end;
dom (doms (GF * ())) = dom (GF * ()) by FUNCT_6:59;
then dom x9 = dom (doms (GF * ())) by ;
then A44: x9 in product (doms (GF * ())) by ;
rng () c= dom F by A5;
then S2: dom (F * ()) = dom () by RELAT_1:27;
S0: dom () = dom x99 by ;
dom Fr = (dom (F * ())) /\ (dom x99) by
.= dom (G * ()) by A9, S0, S2 ;
then dom Fr = dom (doms (G * ())) by FUNCT_6:59;
then Fr in product (doms (G * ())) by ;
then A45: (Frege (G * ())) . ((Frege (F * ())) . x) = (G * ()) .. ((Frege (F * ())) . x) by PRALG_2:def 2
.= Ga .. (Fa .. x99) by
.= (Ga ** Fa) .. x99 by ;
A46: Args (o,U3) <> {} by ;
then GF # x = (Frege (GF * ())) . x by
.= (Frege (G * ())) . ((Frege (F * ())) . x) by
.= (Frege (G * ())) . (F # x) by ;
hence GF # x = G # (F # x) by ; :: thesis: verum