let I be 2 -element set ; :: thesis: for f being ManySortedSet of I
for i, j being Element of I
for x being object st i <> j holds
( f +* (i,x) = (i,j) --> (x,(f . j)) & f +* (j,x) = (i,j) --> ((f . i),x) )
let f be ManySortedSet of I; :: thesis: for i, j being Element of I
for x being object st i <> j holds
( f +* (i,x) = (i,j) --> (x,(f . j)) & f +* (j,x) = (i,j) --> ((f . i),x) )
let i, j be Element of I; :: thesis: for x being object st i <> j holds
( f +* (i,x) = (i,j) --> (x,(f . j)) & f +* (j,x) = (i,j) --> ((f . i),x) )
let x be object ; :: thesis: ( i <> j implies ( f +* (i,x) = (i,j) --> (x,(f . j)) & f +* (j,x) = (i,j) --> ((f . i),x) ) )
assume A1: i <> j ; :: thesis: ( f +* (i,x) = (i,j) --> (x,(f . j)) & f +* (j,x) = (i,j) --> ((f . i),x) )
thus f +* (i,x) = (i,j) --> (x,(f . j)) by A1, Lm2; :: thesis: f +* (j,x) = (i,j) --> ((f . i),x)
thus f +* (j,x) = (j,i) --> (x,(f . i)) by A1, Lm2
.= (i,j) --> ((f . i),x) by A1, Th10 ; :: thesis: verum