let f be Function; :: thesis: for x1, x2 being object st x1 <> x2 holds
rng (renameElementsDistinctlyFunc (f,x1)) misses rng (renameElementsDistinctlyFunc (f,x2))
let x1, x2 be object ; :: thesis: ( x1 <> x2 implies rng (renameElementsDistinctlyFunc (f,x1)) misses rng (renameElementsDistinctlyFunc (f,x2)) )
assume A1: x1 <> x2 ; :: thesis: rng (renameElementsDistinctlyFunc (f,x1)) misses rng (renameElementsDistinctlyFunc (f,x2))
per cases ( ( x1 in dom f & x2 in dom f ) or not x1 in dom f or not x2 in dom f ) ;
suppose A2: ( x1 in dom f & x2 in dom f ) ; :: thesis: rng (renameElementsDistinctlyFunc (f,x1)) misses rng (renameElementsDistinctlyFunc (f,x2))
(rng (renameElementsDistinctlyFunc (f,x1))) /\ (rng (renameElementsDistinctlyFunc (f,x2))) = {}
proof
assume (rng (renameElementsDistinctlyFunc (f,x1))) /\ (rng (renameElementsDistinctlyFunc (f,x2))) <> {} ; :: thesis: contradiction
then consider z being object such that
A3: z in (rng (renameElementsDistinctlyFunc (f,x1))) /\ (rng (renameElementsDistinctlyFunc (f,x2))) by XBOOLE_0:def 1;
A4: ( z in rng (renameElementsDistinctlyFunc (f,x1)) & z in rng (renameElementsDistinctlyFunc (f,x2)) ) by A3, XBOOLE_0:def 4;
then consider y1 being object such that
A5: ( y1 in f . x1 & z = [f,x1,y1] ) by A2, Th79;
consider y2 being object such that
A6: ( y2 in f . x2 & z = [f,x2,y2] ) by A2, A4, Th79;
thus contradiction by A1, A5, A6, XTUPLE_0:3; :: thesis: verum
end;
hence rng (renameElementsDistinctlyFunc (f,x1)) misses rng (renameElementsDistinctlyFunc (f,x2)) by XBOOLE_0:def 7; :: thesis: verum
end;
suppose ( not x1 in dom f or not x2 in dom f ) ; :: thesis: rng (renameElementsDistinctlyFunc (f,x1)) misses rng (renameElementsDistinctlyFunc (f,x2))
then ( f . x1 = {} or f . x2 = {} ) by FUNCT_1:def 2;
then ( renameElementsDistinctlyFunc (f,x1) = {} or renameElementsDistinctlyFunc (f,x2) = {} ) ;
then ( rng (renameElementsDistinctlyFunc (f,x1)) = {} or rng (renameElementsDistinctlyFunc (f,x2)) = {} ) ;
hence rng (renameElementsDistinctlyFunc (f,x1)) misses rng (renameElementsDistinctlyFunc (f,x2)) by XBOOLE_1:65; :: thesis: verum
end;
end;