let I be set ; :: thesis: for A, B being ManySortedSet of I st A is_transformable_to B holds

(Funcs) (A,B) is V2()

let A, B be ManySortedSet of I; :: thesis: ( A is_transformable_to B implies (Funcs) (A,B) is V2() )

assume A1: A is_transformable_to B ; :: thesis: (Funcs) (A,B) is V2()

A2: for i being set st i in I holds

Funcs ((A . i),(B . i)) <> {}

((Funcs) (A,B)) . i <> {}

not ((Funcs) (A,B)) . i is empty ;

hence (Funcs) (A,B) is V2() by PBOOLE:def 13; :: thesis: verum

(Funcs) (A,B) is V2()

let A, B be ManySortedSet of I; :: thesis: ( A is_transformable_to B implies (Funcs) (A,B) is V2() )

assume A1: A is_transformable_to B ; :: thesis: (Funcs) (A,B) is V2()

A2: for i being set st i in I holds

Funcs ((A . i),(B . i)) <> {}

proof

for i being object st i in I holds
let i be set ; :: thesis: ( i in I implies Funcs ((A . i),(B . i)) <> {} )

assume i in I ; :: thesis: Funcs ((A . i),(B . i)) <> {}

then ( B . i = {} implies A . i = {} ) by A1;

hence Funcs ((A . i),(B . i)) <> {} by FUNCT_2:8; :: thesis: verum

end;assume i in I ; :: thesis: Funcs ((A . i),(B . i)) <> {}

then ( B . i = {} implies A . i = {} ) by A1;

hence Funcs ((A . i),(B . i)) <> {} by FUNCT_2:8; :: thesis: verum

((Funcs) (A,B)) . i <> {}

proof

then
for i being object st i in I holds
let i be object ; :: thesis: ( i in I implies ((Funcs) (A,B)) . i <> {} )

assume A3: i in I ; :: thesis: ((Funcs) (A,B)) . i <> {}

then ((Funcs) (A,B)) . i = Funcs ((A . i),(B . i)) by PBOOLE:def 17;

hence ((Funcs) (A,B)) . i <> {} by A2, A3; :: thesis: verum

end;assume A3: i in I ; :: thesis: ((Funcs) (A,B)) . i <> {}

then ((Funcs) (A,B)) . i = Funcs ((A . i),(B . i)) by PBOOLE:def 17;

hence ((Funcs) (A,B)) . i <> {} by A2, A3; :: thesis: verum

not ((Funcs) (A,B)) . i is empty ;

hence (Funcs) (A,B) is V2() by PBOOLE:def 13; :: thesis: verum