let E be non empty set ; :: thesis: for f being Function of VAR,E
for v1 being Element of VAR holds
( decode . (x". v1) = v1 & (decode ") . v1 = x". v1 & (f * decode) . (x". v1) = f . v1 )
let f be Function of VAR,E; :: thesis: for v1 being Element of VAR holds
( decode . (x". v1) = v1 & (decode ") . v1 = x". v1 & (f * decode) . (x". v1) = f . v1 )
let v1 be Element of VAR ; :: thesis: ( decode . (x". v1) = v1 & (decode ") . v1 = x". v1 & (f * decode) . (x". v1) = f . v1 )
thus A1: decode . (x". v1) = x. (card (x". v1)) by Def1
.= x. (x". v1)
.= v1 by Def2 ; :: thesis: ( (decode ") . v1 = x". v1 & (f * decode) . (x". v1) = f . v1 )
hence (decode ") . v1 = x". v1 by Lm1, FUNCT_1:34; :: thesis: (f * decode) . (x". v1) = f . v1
x". v1 in omega ;
then x". v1 in dom (f * decode) by Lm3;
hence (f * decode) . (x". v1) = f . v1 by A1, FUNCT_1:12; :: thesis: verum