let I be 2 -element set ; :: thesis: for f being ManySortedSet of I

for i, j being Element of I st i <> j holds

f = (i,j) --> ((f . i),(f . j))

let f be ManySortedSet of I; :: thesis: for i, j being Element of I st i <> j holds

f = (i,j) --> ((f . i),(f . j))

let i, j be Element of I; :: thesis: ( i <> j implies f = (i,j) --> ((f . i),(f . j)) )

assume A1: i <> j ; :: thesis: f = (i,j) --> ((f . i),(f . j))

dom f = I by PARTFUN1:def 2

.= {i,j} by A1, Th8 ;

hence f = (i,j) --> ((f . i),(f . j)) by FUNCT_4:66; :: thesis: verum

for i, j being Element of I st i <> j holds

f = (i,j) --> ((f . i),(f . j))

let f be ManySortedSet of I; :: thesis: for i, j being Element of I st i <> j holds

f = (i,j) --> ((f . i),(f . j))

let i, j be Element of I; :: thesis: ( i <> j implies f = (i,j) --> ((f . i),(f . j)) )

assume A1: i <> j ; :: thesis: f = (i,j) --> ((f . i),(f . j))

dom f = I by PARTFUN1:def 2

.= {i,j} by A1, Th8 ;

hence f = (i,j) --> ((f . i),(f . j)) by FUNCT_4:66; :: thesis: verum