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))
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))
let i, j be Element of I; :: thesis: for x being object st i <> j holds
f +* (i,x) = (i,j) --> (x,(f . j))
let x be object ; :: thesis: ( i <> j implies f +* (i,x) = (i,j) --> (x,(f . j)) )
assume A1: i <> j ; :: thesis: f +* (i,x) = (i,j) --> (x,(f . j))
then a2: I = {i,j} by Th8;
then A2: dom f = {i,j} by PARTFUN1:def 2;
A3: dom (f +* (i,x)) = dom f by FUNCT_7:30
.= dom ((i,j) --> (x,(f . j))) by A2, FUNCT_4:62 ;
for z being object st z in dom (f +* (i,x)) holds
(f +* (i,x)) . z = ((i,j) --> (x,(f . j))) . z

proof

let z be object ; :: thesis: ( z in dom (f +* (i,x)) implies (f +* (i,x)) . z = ((i,j) --> (x,(f . j))) . z )
assume z in dom (f +* (i,x)) ; :: thesis: (f +* (i,x)) . z = ((i,j) --> (x,(f . j))) . z

per cases then ( z = i or z = j ) by a2, TARSKI:def 2;

suppose A5: z = i ; :: thesis: (f +* (i,x)) . z = ((i,j) --> (x,(f . j))) . z

hence (f +* (i,x)) . z = x by A2, a2, FUNCT_7:31
.= ((i,j) --> (x,(f . j))) . z by A1, A5, FUNCT_4:63 ;
:: thesis: verum

end;

suppose A6: z = j ; :: thesis: (f +* (i,x)) . z = ((i,j) --> (x,(f . j))) . z

hence (f +* (i,x)) . z = f . j by A1, FUNCT_7:32
.= ((i,j) --> (x,(f . j))) . z by A6, FUNCT_4:63 ;
:: thesis: verum

end;

end;

end;

hence f +* (i,x) = (i,j) --> (x,(f . j)) by A3, FUNCT_1:2; :: thesis: verum