let H be ZF-formula; :: thesis: for M being non empty set
for m being Element of M
for v being Function of VAR ,M
for i being Element of NAT st x. i in Free H holds
{[i,m]} \/ ((v * decode ) | ((code (Free H)) \ {i})) = ((v / (x. i),m) * decode ) | (code (Free H))
let M be non empty set ; :: thesis: for m being Element of M
for v being Function of VAR ,M
for i being Element of NAT st x. i in Free H holds
{[i,m]} \/ ((v * decode ) | ((code (Free H)) \ {i})) = ((v / (x. i),m) * decode ) | (code (Free H))
let m be Element of M; :: thesis: for v being Function of VAR ,M
for i being Element of NAT st x. i in Free H holds
{[i,m]} \/ ((v * decode ) | ((code (Free H)) \ {i})) = ((v / (x. i),m) * decode ) | (code (Free H))
let v be Function of VAR ,M; :: thesis: for i being Element of NAT st x. i in Free H holds
{[i,m]} \/ ((v * decode ) | ((code (Free H)) \ {i})) = ((v / (x. i),m) * decode ) | (code (Free H))
let i be Element of NAT ; :: thesis: ( x. i in Free H implies {[i,m]} \/ ((v * decode ) | ((code (Free H)) \ {i})) = ((v / (x. i),m) * decode ) | (code (Free H)) )
set e = (v / (x. i),m) * decode ;
set f = v * decode ;
set b = (v * decode ) | ((code (Free H)) \ {i});
assume
x. i in Free H
; :: thesis: {[i,m]} \/ ((v * decode ) | ((code (Free H)) \ {i})) = ((v / (x. i),m) * decode ) | (code (Free H))
then
x". (x. i) in code (Free H)
by ZF_FUND1:34;
then
i in code (Free H)
by ZF_FUND1:def 3;
then A1:
{i} c= code (Free H)
by ZFMISC_1:37;
A2:
i in {i}
by TARSKI:def 1;
A3: dom (((v / (x. i),m) * decode ) | {i}) =
(dom ((v / (x. i),m) * decode )) /\ {i}
by RELAT_1:90
.=
omega /\ {i}
by ZF_FUND1:32
.=
{i}
by ZFMISC_1:52
;
then A4: ((v / (x. i),m) * decode ) | {i} =
{[i,((((v / (x. i),m) * decode ) | {i}) . i)]}
by GRFUNC_1:18
.=
{[i,(((v / (x. i),m) * decode ) . i)]}
by A2, A3, FUNCT_1:70
.=
{[i,(((v / (x. i),m) * decode ) . (x". (x. i)))]}
by ZF_FUND1:def 3
.=
{[i,((v / (x. i),m) . (x. i))]}
by ZF_FUND1:33
.=
{[i,m]}
by FUNCT_7:130
;
A5:
(v * decode ) | ((code (Free H)) \ {i}) = ((v / (x. i),m) * decode ) | ((code (Free H)) \ {i})
proof
A6:
dom ((v * decode ) | ((code (Free H)) \ {i})) =
(dom (v * decode )) /\ ((code (Free H)) \ {i})
by RELAT_1:90
.=
omega /\ ((code (Free H)) \ {i})
by ZF_FUND1:32
.=
(dom ((v / (x. i),m) * decode )) /\ ((code (Free H)) \ {i})
by ZF_FUND1:32
.=
dom (((v / (x. i),m) * decode ) | ((code (Free H)) \ {i}))
by RELAT_1:90
;
now let u be
set ;
:: thesis: ( u in dom ((v * decode ) | ((code (Free H)) \ {i})) implies ((v * decode ) | ((code (Free H)) \ {i})) . u = (((v / (x. i),m) * decode ) | ((code (Free H)) \ {i})) . u )assume A7:
u in dom ((v * decode ) | ((code (Free H)) \ {i}))
;
:: thesis: ((v * decode ) | ((code (Free H)) \ {i})) . u = (((v / (x. i),m) * decode ) | ((code (Free H)) \ {i})) . uthen
u in (dom (v * decode )) /\ ((code (Free H)) \ {i})
by RELAT_1:90;
then
u in (code (Free H)) \ {i}
by XBOOLE_0:def 4;
then A8:
(
u in code (Free H) & not
u in {i} )
by XBOOLE_0:def 5;
then consider x being
Variable such that A9:
(
x in Free H &
u = x". x )
by ZF_FUND1:34;
i <> x". x
by A8, A9, TARSKI:def 1;
then A10:
x <> x. i
by ZF_FUND1:def 3;
thus ((v * decode ) | ((code (Free H)) \ {i})) . u =
(v * decode ) . u
by A7, FUNCT_1:70
.=
v . x
by A9, ZF_FUND1:33
.=
(v / (x. i),m) . x
by A10, FUNCT_7:34
.=
((v / (x. i),m) * decode ) . u
by A9, ZF_FUND1:33
.=
(((v / (x. i),m) * decode ) | ((code (Free H)) \ {i})) . u
by A6, A7, FUNCT_1:70
;
:: thesis: verum end;
hence
(v * decode ) | ((code (Free H)) \ {i}) = ((v / (x. i),m) * decode ) | ((code (Free H)) \ {i})
by A6, FUNCT_1:9;
:: thesis: verum
end;
((v / (x. i),m) * decode ) | (code (Free H)) =
((v / (x. i),m) * decode ) | ({i} \/ ((code (Free H)) \ {i}))
by A1, XBOOLE_1:45
.=
{[i,m]} \/ ((v * decode ) | ((code (Free H)) \ {i}))
by A4, A5, RELAT_1:107
;
hence
{[i,m]} \/ ((v * decode ) | ((code (Free H)) \ {i})) = ((v / (x. i),m) * decode ) | (code (Free H))
; :: thesis: verum