let x, y be ManySortedFunction of ([|A,B|] #) * p,[|A,B|] * r; ( ( for j being object st j in J holds
for pj being Element of I *
for rj being Element of I st pj = p . j & rj = r . j holds
for f being Function of ((A #) . pj),(A . rj)
for g being Function of ((B #) . pj),(B . rj) st f = F . j & g = G . j holds
x . j = [[:f,g:]] ) & ( for j being object st j in J holds
for pj being Element of I *
for rj being Element of I st pj = p . j & rj = r . j holds
for f being Function of ((A #) . pj),(A . rj)
for g being Function of ((B #) . pj),(B . rj) st f = F . j & g = G . j holds
y . j = [[:f,g:]] ) implies x = y )
assume that
A20:
for j being object st j in J holds
for pj being Element of I *
for rj being Element of I st pj = p . j & rj = r . j holds
for f being Function of ((A #) . pj),(A . rj)
for g being Function of ((B #) . pj),(B . rj) st f = F . j & g = G . j holds
x . j = [[:f,g:]]
and
A21:
for j being object st j in J holds
for pj being Element of I *
for rj being Element of I st pj = p . j & rj = r . j holds
for f being Function of ((A #) . pj),(A . rj)
for g being Function of ((B #) . pj),(B . rj) st f = F . j & g = G . j holds
y . j = [[:f,g:]]
; x = y
for j being object st j in J holds
x . j = y . j
proof
let j be
object ;
( j in J implies x . j = y . j )
assume A22:
j in J
;
x . j = y . j
then reconsider pj =
p . j as
Element of
I * by FUNCT_2:5;
reconsider rj =
r . j as
Element of
I by A22, FUNCT_2:5;
A23:
j in dom r
by A22, FUNCT_2:def 1;
then A24:
A . (r . j) = (A * r) . j
by FUNCT_1:13;
A25:
B . (r . j) = (B * r) . j
by A23, FUNCT_1:13;
A26:
j in dom p
by A22, FUNCT_2:def 1;
then
(A #) . (p . j) = ((A #) * p) . j
by FUNCT_1:13;
then reconsider f =
F . j as
Function of
((A #) . pj),
(A . rj) by A22, A24, PBOOLE:def 15;
(B #) . (p . j) = ((B #) * p) . j
by A26, FUNCT_1:13;
then reconsider g =
G . j as
Function of
((B #) . pj),
(B . rj) by A22, A25, PBOOLE:def 15;
x . j = [[:f,g:]]
by A20, A22;
hence
x . j = y . j
by A21, A22;
verum
end;
hence
x = y
; verum