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 ;

then A19: Fr = (F * (the_arity_of o)) .. x9 by PRALG_2:def 2;

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

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;

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

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

then A18:
x9 in product (doms (F * (the_arity_of o)))
by A8, CARD_3:9;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

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

end;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
end;

(F * (the_arity_of o)) . x = F . ((the_arity_of o) . x)
by A14, FUNCT_1:13;per cases
( the Sorts of U2 . ((the_arity_of o) . x) <> {} or the Sorts of U2 . ((the_arity_of o) . x) = {} )
;

end;

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

end;

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;hence the Sorts of U1 . ((the_arity_of o) . x) = dom Ff ; :: thesis: verum

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

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

reconsider GF = G ** F as ManySortedFunction of U1,U3 by A2, ALTCAT_2:4;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 Z4: (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)

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;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 Z4: (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
end;

A29:
the Sorts of U1 . ((the_arity_of o) . x) = dom Ff
per cases
( the Sorts of U3 . ((the_arity_of o) . x) <> {} or the Sorts of U3 . ((the_arity_of o) . x) = {} )
;

end;

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

end;

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;hence dom Gds = the Sorts of U2 . ((the_arity_of o) . x) ; :: thesis: verum

proof
end;

( the Sorts of U1 * (the_arity_of o)) . x = the Sorts of U1 . ((the_arity_of o) . x)
by A25, FUNCT_1:13;per cases
( the Sorts of U2 . ((the_arity_of o) . x) <> {} or the Sorts of U2 . ((the_arity_of o) . x) = {} )
;

end;

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

end;

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;hence the Sorts of U1 . ((the_arity_of o) . x) = dom Ff ; :: thesis: verum

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

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

take
GF
; :: thesis: ( GF = G ** F & GF # x = G # (F # x) )
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)

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;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
end;

i in dom ( the Sorts of U1 * (the_arity_of o))
by A33, PRALG_2:3;per cases
( the Sorts of U2 . ((the_arity_of o) . i) = {} or the Sorts of U2 . ((the_arity_of o) . i) <> {} )
;

end;

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;hence dom Ew = the Sorts of U1 . ((the_arity_of o) . i) ; :: thesis: verum

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

end;

end;

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

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

dom (doms (GF * (the_arity_of o))) = dom (GF * (the_arity_of o))
by FUNCT_6:59;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

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;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
end;

x in dom ( the Sorts of U1 * (the_arity_of o))
by A11, A40, RELAT_1:27;per cases
( the Sorts of U3 . ((the_arity_of o) . x) <> {} or the Sorts of U3 . ((the_arity_of o) . x) = {} )
;

end;

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

end;

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;hence the Sorts of U1 . ((the_arity_of o) . x) = dom Gf ; :: thesis: verum

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

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