let S be non empty non void ManySortedSign ; :: thesis:
let o be OperSymbol of S; :: thesis:
let U1, U2, U3 be feasible MSAlgebra of S; :: thesis:
let F be ManySortedFunction of U1,U2; :: thesis:
let G be ManySortedFunction of U2,U3; :: thesis:
let x be Element of Args o,U1; :: thesis:
assume A1: ( 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 ) ; :: thesis:
then A2: the Sorts of U1 is_transformable_to the Sorts of U3 by AUTALG_1:11;
reconsider GF = G ** F as ManySortedFunction of U1,U3 by A1, ALTCAT_2:4;
A3: ( Args o,U2 <> {} & Args o,U3 <> {} ) by A1, Th3, AUTALG_1:11;
take GF ; :: thesis:
thus GF = G ** F ; :: thesis:
x in Args o,U1 by A1;
then x in product (the Sorts of U1 * (the_arity_of o)) by PRALG_2:10;
then consider g being Function such that
A4: ( x = g & dom g = dom (the Sorts of U1 * (the_arity_of o)) & ( for x being set 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;
reconsider x' = x as Function by A4;
A5: dom GF = the carrier of S by PARTFUN1:def 4;
dom G = the carrier of S by PARTFUN1:def 4;
then rng (the_arity_of o) c= dom G ;
then A6: dom (G * (the_arity_of o)) = dom (the_arity_of o) by RELAT_1:46;
rng (the_arity_of o) c= dom GF by A5;
then A7: dom (GF * (the_arity_of o)) = dom (the_arity_of o) by RELAT_1:46;
dom the Sorts of U1 = the carrier of S by PARTFUN1:def 4;
then A8: rng (the_arity_of o) c= dom the Sorts of U1 ;
dom (doms (GF * (the_arity_of o))) = dom (GF * (the_arity_of o)) by FUNCT_6:89;
then A9: dom x' = dom (doms (GF * (the_arity_of o))) by A1, A7, MSUALG_3:6;

now

let x be set ; :: thesis:
assume A10: x in dom (doms (GF * (the_arity_of o))) ; :: thesis:
then x in dom (GF * (the_arity_of o)) by FUNCT_6:89;
then A11: (doms (GF * (the_arity_of o))) . x = dom ((GF * (the_arity_of o)) . x) by FUNCT_6:31;
A12: x in dom (the_arity_of o) by A7, A10, FUNCT_6:89;
then x in dom (the Sorts of U1 * (the_arity_of o)) by A8, RELAT_1:46;
then A13: x' . x in (the Sorts of U1 * (the_arity_of o)) . x by A1, MSUALG_3:6;
set ds = (the_arity_of o) . x;
A14: (the_arity_of o) . x in rng (the_arity_of o) by A12, FUNCT_1:def 5;
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 18;
the Sorts of U1 . ((the_arity_of o) . x) = dom Gf

proof

per cases ;

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

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

end;

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

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

end;

then x' . x in dom (GF . ((the_arity_of o) . x)) by A12, A13, FUNCT_1:23;
hence x' . x in (doms (GF * (the_arity_of o))) . x by A11, A12, FUNCT_1:23; :: thesis:

end;

then A15: x' in product (doms (GF * (the_arity_of o))) by A9, CARD_3:18;
dom F = the carrier of S by PARTFUN1:def 4;
then A16: rng (the_arity_of o) c= dom F ;
then A17: dom (F * (the_arity_of o)) = dom (the_arity_of o) by RELAT_1:46;
A18: dom (doms (F * (the_arity_of o))) = dom (F * (the_arity_of o)) by FUNCT_6:89;
then A19: dom x' = dom (doms (F * (the_arity_of o))) by A1, A17, MSUALG_3:6;

now

let x be set ; :: thesis:
assume x in dom (doms (F * (the_arity_of o))) ; :: thesis:
then A20: x in dom (F * (the_arity_of o)) by FUNCT_6:89;
then A21: (doms (F * (the_arity_of o))) . x = dom ((F * (the_arity_of o)) . x) by FUNCT_6:31;
A22: x in dom (the_arity_of o) by A16, A20, RELAT_1:46;
then x in dom (the Sorts of U1 * (the_arity_of o)) by A8, RELAT_1:46;
then A23: x' . x in (the Sorts of U1 * (the_arity_of o)) . x by A1, MSUALG_3:6;
set ds = (the_arity_of o) . x;
A24: (the_arity_of o) . x in rng (the_arity_of o) by A22, FUNCT_1:def 5;
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 18;
A25: the Sorts of U1 . ((the_arity_of o) . x) = dom Ff

proof

per cases ;

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

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

end;

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

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

end;

(F * (the_arity_of o)) . x = F . ((the_arity_of o) . x) by A22, FUNCT_1:23;
hence x' . x in (doms (F * (the_arity_of o))) . x by A21, A22, A23, A25, FUNCT_1:23; :: thesis:

end;

then A26: x' in product (doms (F * (the_arity_of o))) by A19, CARD_3:18;
reconsider Fr = (Frege (F * (the_arity_of o))) . x' as Function ;
A27: Fr = (F * (the_arity_of o)) .. x' by A26, PRALG_2:def 8;
then dom Fr = dom (G * (the_arity_of o)) by A6, A17, PRALG_1:def 17;
then A28: dom Fr = dom (doms (G * (the_arity_of o))) by FUNCT_6:89;

now

let x be set ; :: thesis:
assume A29: x in dom (doms (G * (the_arity_of o))) ; :: thesis:
then A30: x in dom (G * (the_arity_of o)) by FUNCT_6:89;
A31: x in dom (the_arity_of o) by A6, A29, FUNCT_6:89;
A32: dom (the Sorts of U1 * (the_arity_of o)) = dom (the_arity_of o) by A8, RELAT_1:46;
A33: (the Sorts of U1 * (the_arity_of o)) . x = the Sorts of U1 . ((the_arity_of o) . x) by A31, FUNCT_1:23;
set ds = (the_arity_of o) . x;
A34: (the_arity_of o) . x in rng (the_arity_of o) by A31, FUNCT_1:def 5;
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 18;
A35: the Sorts of U1 . ((the_arity_of o) . x) = dom Ff

proof

per cases ;

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

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

end;

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

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

end;

A36: (G * (the_arity_of o)) . x = G . ((the_arity_of o) . x) by A31, FUNCT_1:23;
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 A34, PBOOLE:def 18;
A37: dom Gds = the Sorts of U2 . ((the_arity_of o) . x)

proof

per cases ;

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

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

end;

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

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

end;

A38: x in dom (F * (the_arity_of o)) by A6, A17, A29, FUNCT_6:89;
A39: (F * (the_arity_of o)) . x = Ff by A17, A31, FUNCT_1:22;
x' . x in dom Ff by A1, A31, A32, A33, A35, MSUALG_3:6;
then A40: ((F * (the_arity_of o)) . x) . (x' . x) in rng Ff by A39, FUNCT_1:def 5;
Fr . x = ((F * (the_arity_of o)) . x) . (x' . x) by A27, A38, PRALG_1:def 17;
then Fr . x in dom ((G * (the_arity_of o)) . x) by A36, A37, A40;
hence Fr . x in (doms (G * (the_arity_of o))) . x by A30, FUNCT_6:31; :: thesis:

end;

then A41: Fr in product (doms (G * (the_arity_of o))) by A28, CARD_3:18;
reconsider x'' = x' as ManySortedSet of by A17, A18, A19, PARTFUN1:def 4, RELAT_1:def 18;
reconsider Ga = G * (the_arity_of o), Fa = F * (the_arity_of o) as ManySortedFunction of by A6, A17, PARTFUN1:def 4, RELAT_1:def 18;
A42: x'' in doms Fa

proof

let i be set ; :: according to PBOOLE:def 4 :: thesis:
assume A43: i in dom (the_arity_of o) ; :: thesis:
then A44: Fa . i = F . ((the_arity_of o) . i) by FUNCT_1:23;
set ai = (the_arity_of o) . i;
A45: (the_arity_of o) . i in rng (the_arity_of o) by A43, FUNCT_1:def 5;
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 A44, PBOOLE:def 18;
A46: dom Ew = the Sorts of U1 . ((the_arity_of o) . i)

proof

per cases ;

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

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

end;

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

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

end;

i in dom (the Sorts of U1 * (the_arity_of o)) by A43, PRALG_2:10;
then x'' . i in (the Sorts of U1 * (the_arity_of o)) . i by A4;
then x'' . i in dom (Fa . i) by A43, A46, FUNCT_1:23;
hence x'' . i in (doms Fa) . i by A43, MSSUBFAM:14; :: thesis:

end;

A47: (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 A41, PRALG_2:def 8
.= Ga .. (Fa .. x'') by A26, PRALG_2:def 8
.= (Ga ** Fa) .. x'' by A42, CLOSURE1:4 ;
A48: (G * (the_arity_of o)) ** (F * (the_arity_of o)) = GF * (the_arity_of o) by FUNCTOR0:13;
GF # x = (Frege (GF * (the_arity_of o))) . x by A1, A3, MSUALG_3:def 7
.= (Frege (G * (the_arity_of o))) . ((Frege (F * (the_arity_of o))) . x) by A15, A47, A48, PRALG_2:def 8
.= (Frege (G * (the_arity_of o))) . (F # x) by A1, A3, MSUALG_3:def 7 ;
hence GF # x = G # (F # x) by A3, MSUALG_3:def 7; :: thesis: