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});
A1: i in {i} by TARSKI:def 1;
A2: dom (((v / ((x. i),m)) * decode) | {i}) = (dom ((v / ((x. i),m)) * decode)) /\ {i} by RELAT_1:61
.= omega /\ {i} by ZF_FUND1:31
.= {i} by ZFMISC_1:46 ;
then A3: ((v / ((x. i),m)) * decode) | {i} = {[i,((((v / ((x. i),m)) * decode) | {i}) . i)]} by GRFUNC_1:7
.= {[i,(((v / ((x. i),m)) * decode) . i)]} by A1, A2, FUNCT_1:47
.= {[i,(((v / ((x. i),m)) * decode) . (x". (x. i)))]} by ZF_FUND1:def 3
.= {[i,((v / ((x. i),m)) . (x. i))]} by ZF_FUND1:32
.= {[i,m]} by FUNCT_7:128 ;
A4: dom ((v * decode) | ((code (Free H)) \ {i})) = (dom (v * decode)) /\ ((code (Free H)) \ {i}) by RELAT_1:61
.= omega /\ ((code (Free H)) \ {i}) by ZF_FUND1:31
.= (dom ((v / ((x. i),m)) * decode)) /\ ((code (Free H)) \ {i}) by ZF_FUND1:31
.= dom (((v / ((x. i),m)) * decode) | ((code (Free H)) \ {i})) by RELAT_1:61 ;

now :: thesis: for u being object st u in dom ((v * decode) | ((code (Free H)) \ {i})) holds
((v * decode) | ((code (Free H)) \ {i})) . u = (((v / ((x. i),m)) * decode) | ((code (Free H)) \ {i})) . u

let u be object ; :: 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 A5: 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})) . u
then u in (dom (v * decode)) /\ ((code (Free H)) \ {i}) by RELAT_1:61;
then A6: u in (code (Free H)) \ {i} by XBOOLE_0:def 4;
then u in code (Free H) by XBOOLE_0:def 5;
then consider x being Variable such that
x in Free H and
A7: u = x". x by ZF_FUND1:33;
not u in {i} by A6, XBOOLE_0:def 5;
then i <> x". x by A7, TARSKI:def 1;
then A8: x <> x. i by ZF_FUND1:def 3;
thus ((v * decode) | ((code (Free H)) \ {i})) . u = (v * decode) . u by A5, FUNCT_1:47
.= v . x by A7, ZF_FUND1:32
.= (v / ((x. i),m)) . x by A8, FUNCT_7:32
.= ((v / ((x. i),m)) * decode) . u by A7, ZF_FUND1:32
.= (((v / ((x. i),m)) * decode) | ((code (Free H)) \ {i})) . u by A4, A5, FUNCT_1:47 ; :: thesis: verum

end;

then A9: (v * decode) | ((code (Free H)) \ {i}) = ((v / ((x. i),m)) * decode) | ((code (Free H)) \ {i}) by A4, FUNCT_1:2;
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:33;
then i in code (Free H) by ZF_FUND1:def 3;
then {i} c= code (Free H) by ZFMISC_1:31;
then ((v / ((x. i),m)) * decode) | (code (Free H)) = ((v / ((x. i),m)) * decode) | ({i} \/ ((code (Free H)) \ {i})) by XBOOLE_1:45
.= {[i,m]} \/ ((v * decode) | ((code (Free H)) \ {i})) by A3, A9, RELAT_1:78 ;
hence {[i,m]} \/ ((v * decode) | ((code (Free H)) \ {i})) = ((v / ((x. i),m)) * decode) | (code (Free H)) ; :: thesis: verum