let I be non empty set ; :: thesis: for A, B, f being ManySortedSet of I holds
( f is ManySortedFunction of A,B iff for i being Element of I holds f . i is Function of (A . i),(B . i) )
let A, B be ManySortedSet of I; :: thesis: for f being ManySortedSet of I holds
( f is ManySortedFunction of A,B iff for i being Element of I holds f . i is Function of (A . i),(B . i) )
let f be ManySortedSet of I; :: thesis: ( f is ManySortedFunction of A,B iff for i being Element of I holds f . i is Function of (A . i),(B . i) )
thus ( f is ManySortedFunction of A,B implies for i being Element of I holds f . i is Function of (A . i),(B . i) ) by PBOOLE:def 15; :: thesis: ( ( for i being Element of I holds f . i is Function of (A . i),(B . i) ) implies f is ManySortedFunction of A,B )
assume for i being Element of I holds f . i is Function of (A . i),(B . i) ; :: thesis: f is ManySortedFunction of A,B
then for i being object st i in I holds
f . i is Function of (A . i),(B . i) ;
hence f is ManySortedFunction of A,B by PBOOLE:def 15; :: thesis: verum