let I1, I2 be non empty set ; :: thesis: for A being ManySortedSet of I1
for B being ManySortedSet of I2
for o being Element of I2 st B . o <> {} holds
for m being Element of B . o
for f being Function of I1,I2 st f = I1 --> o holds
{ [o9,((A . o9) --> m)] where o9 is Element of I1 : verum } is MSUnTrans of f,A,B
let A be ManySortedSet of I1; :: thesis: for B being ManySortedSet of I2
for o being Element of I2 st B . o <> {} holds
for m being Element of B . o
for f being Function of I1,I2 st f = I1 --> o holds
{ [o9,((A . o9) --> m)] where o9 is Element of I1 : verum } is MSUnTrans of f,A,B
let B be ManySortedSet of I2; :: thesis: for o being Element of I2 st B . o <> {} holds
for m being Element of B . o
for f being Function of I1,I2 st f = I1 --> o holds
{ [o9,((A . o9) --> m)] where o9 is Element of I1 : verum } is MSUnTrans of f,A,B
let o be Element of I2; :: thesis: ( B . o <> {} implies for m being Element of B . o
for f being Function of I1,I2 st f = I1 --> o holds
{ [o9,((A . o9) --> m)] where o9 is Element of I1 : verum } is MSUnTrans of f,A,B )
assume A1: B . o <> {} ; :: thesis: for m being Element of B . o
for f being Function of I1,I2 st f = I1 --> o holds
{ [o9,((A . o9) --> m)] where o9 is Element of I1 : verum } is MSUnTrans of f,A,B
let m be Element of B . o; :: thesis: for f being Function of I1,I2 st f = I1 --> o holds
{ [o9,((A . o9) --> m)] where o9 is Element of I1 : verum } is MSUnTrans of f,A,B
let f be Function of I1,I2; :: thesis: ( f = I1 --> o implies { [o9,((A . o9) --> m)] where o9 is Element of I1 : verum } is MSUnTrans of f,A,B )
assume A2: f = I1 --> o ; :: thesis: { [o9,((A . o9) --> m)] where o9 is Element of I1 : verum } is MSUnTrans of f,A,B
defpred S₁[ set ] means verum;
deffunc H₁( set ) -> Element of bool [:(A . $1),{m}:] = (A . $1) --> m;
reconsider Xm = { [o9,H₁(o9)] where o9 is Element of I1 : S₁[o9] } as Function from ALTCAT_2:sch 1();
A3: Xm = { [o9,H₁(o9)] where o9 is Element of I1 : S₁[o9] } ;
dom Xm = { o9 where o9 is Element of I1 : S₁[o9] } from ALTCAT_2:sch 2(A3)
.= I1 by DOMAIN_1:18 ;
then reconsider Xm = Xm as ManySortedSet of I1 by PARTFUN1:def 2, RELAT_1:def 18;
deffunc H₂( set ) -> Element of bool [:(A . $1),{m}:] = (A . $1) --> m;
A4: Xm = { [o9,H₂(o9)] where o9 is Element of I1 : S₁[o9] } ;

now :: thesis: for i being object st i in I1 holds
Xm . i is Function of (A . i),((B * f) . i)

let i be object ; :: thesis: ( i in I1 implies Xm . i is Function of (A . i),((B * f) . i) )
assume A5: i in I1 ; :: thesis: Xm . i is Function of (A . i),((B * f) . i)
then reconsider o9 = i as Element of I1 ;
A6: S₁[o9] ;
A7: i in dom f by A2, A5;
f . i = o by A2, A5, FUNCOP_1:7;
then m in B . (f . i) by A1;
then A8: m in (B * f) . i by A7, FUNCT_1:13;
Xm . o9 = H₂(o9) from ALTCAT_2:sch 3(A4, A6);
hence Xm . i is Function of (A . i),((B * f) . i) by A8, FUNCOP_1:45; :: thesis: verum

end;

then Xm is ManySortedFunction of A,B * f by PBOOLE:def 15;
hence { [o9,((A . o9) --> m)] where o9 is Element of I1 : verum } is MSUnTrans of f,A,B by Def4; :: thesis: verum