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

proof

now

let i be set ; :: 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 o' = i as Element of I1 ;
A6: S₁[o'] ;
A7: i in dom f by A2, A5, FUNCOP_1:19;
f . i = o by A2, A5, FUNCOP_1:13;
then m in B . (f . i) by A1;
then A8: m in (B * f) . i by A7, FUNCT_1:23;
Xm . o' = H₂(o') from ALTCAT_2:sch 3(A4, A6);
hence Xm . i is Function of (A . i),((B * f) . i) by A8, FUNCOP_1:57; :: thesis: verum

end;

hence Xm is ManySortedFunction of A,B * f by PBOOLE:def 18; :: according to FUNCTOR0:def 5 :: thesis: verum

end;

hence { [o',((A . o') --> m)] where o' is Element of I1 : verum } is MSUnTrans of f,A,B ; :: thesis: verum