let f be Function; :: thesis: for X, Y being set
for i being object st X c= Y holds
product (f +* (i .--> X)) c= product (f +* (i .--> Y))
let X, Y be set ; :: thesis: for i being object st X c= Y holds
product (f +* (i .--> X)) c= product (f +* (i .--> Y))
let i be object ; :: thesis: ( X c= Y implies product (f +* (i .--> X)) c= product (f +* (i .--> Y)) )
assume A1: X c= Y ; :: thesis: product (f +* (i .--> X)) c= product (f +* (i .--> Y))
dom (f +* (i .--> X)) = (dom f) \/ (dom (i .--> X)) by FUNCT_4:def 1
.= (dom f) \/ (dom ({i} --> X)) by FUNCOP_1:def 9
.= (dom f) \/ {i} ;
then A3: dom (f +* (i .--> X)) = (dom f) \/ (dom ({i} --> Y))
.= (dom f) \/ (dom (i .--> Y)) by FUNCOP_1:def 9
.= dom (f +* (i .--> Y)) by FUNCT_4:def 1 ;
now :: thesis: for x being object st x in dom (f +* (i .--> X)) holds
(f +* (i .--> X)) . x c= (f +* (i .--> Y)) . x
let x be object ; :: thesis: ( x in dom (f +* (i .--> X)) implies (f +* (i .--> X)) . b1 c= (f +* (i .--> Y)) . b1 )
assume x in dom (f +* (i .--> X)) ; :: thesis: (f +* (i .--> X)) . b1 c= (f +* (i .--> Y)) . b1
per cases ( x = i or x <> i ) ;
suppose A4: x = i ; :: thesis: (f +* (i .--> X)) . b1 c= (f +* (i .--> Y)) . b1
then x in {i} by TARSKI:def 1;
then ( x in dom ({i} --> X) & x in dom ({i} --> Y) ) ;
then A5: ( x in dom (i .--> X) & x in dom (i .--> Y) ) by FUNCOP_1:def 9;
then A6: (f +* (i .--> X)) . x = (i .--> X) . x by FUNCT_4:13
.= X by A4, FUNCOP_1:72 ;
(f +* (i .--> Y)) . x = (i .--> Y) . x by A5, FUNCT_4:13
.= Y by A4, FUNCOP_1:72 ;
hence (f +* (i .--> X)) . x c= (f +* (i .--> Y)) . x by A1, A6; :: thesis: verum
end;
suppose x <> i ; :: thesis: (f +* (i .--> X)) . b1 c= (f +* (i .--> Y)) . b1
then ( not x in dom (i .--> X) & not x in dom (i .--> Y) ) by TARSKI:def 1;
then ( (f +* (i .--> X)) . x = f . x & (f +* (i .--> Y)) . x = f . x ) by FUNCT_4:11;
hence (f +* (i .--> X)) . x c= (f +* (i .--> Y)) . x ; :: thesis: verum
end;
end;
end;
hence product (f +* (i .--> X)) c= product (f +* (i .--> Y)) by A3, CARD_3:27; :: thesis: verum