let x, y be ManySortedFunction of ([|A,B|] # ) * p,[|A,B|] * r; :: thesis: ( ( for j being set 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 set 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
A6: for j being set 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
A7: for j being set 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:]] ; :: thesis: x = y
for j being set st j in J holds
x . j = y . j

proof

let j be set ; :: thesis: ( j in J implies x . j = y . j )
assume A8: j in J ; :: thesis: x . j = y . j
then X: ( j in dom p & j in dom r ) by FUNCT_2:def 1;
reconsider pj = p . j as Element of I * by A8, FUNCT_2:7;
reconsider rj = r . j as Element of I by A8, FUNCT_2:7;
( (A # ) . (p . j) = ((A # ) * p) . j & A . (r . j) = (A * r) . j ) by X, FUNCT_1:23;
then reconsider f = F . j as Function of ((A # ) . pj),(A . rj) by A8, PBOOLE:def 18;
( (B # ) . (p . j) = ((B # ) * p) . j & B . (r . j) = (B * r) . j ) by X, FUNCT_1:23;
then reconsider g = G . j as Function of ((B # ) . pj),(B . rj) by A8, PBOOLE:def 18;
( x . j = [[:f,g:]] & y . j = [[:f,g:]] ) by A6, A7, A8;
hence x . j = y . j ; :: thesis: verum

end;

hence x = y by PBOOLE:3; :: thesis: verum