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