let X be set ; :: thesis: for Y being Subset of X holds rng ((id X) | Y) = Y
let Y be Subset of X; :: thesis: rng ((id X) | Y) = Y
set f = id X;
A1: (id X) | Y is Function of Y,X by FUNCT_2:32;
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: Y c= rng ((id X) | Y)
let y be object ; :: thesis: ( y in rng ((id X) | Y) implies y in Y )
assume y in rng ((id X) | Y) ; :: thesis: y in Y
then consider x being object such that
A2: x in dom ((id X) | Y) and
A3: y = ((id X) | Y) . x by FUNCT_1:def 3;
((id X) | Y) . x = (id X) . x by A2, FUNCT_1:47
.= x by A2, FUNCT_1:17 ;
hence y in Y by A1, A2, A3, FUNCT_2:def 1; :: thesis: verum
end;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Y or y in rng ((id X) | Y) )
( X = {} implies Y = {} ) ;
then A4: dom ((id X) | Y) = Y by A1, FUNCT_2:def 1;
assume A5: y in Y ; :: thesis: y in rng ((id X) | Y)
then ((id X) | Y) . y = (id X) . y by FUNCT_1:49
.= y by A5, FUNCT_1:18 ;
hence y in rng ((id X) | Y) by A4, A5, FUNCT_1:def 3; :: thesis: verum