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 )
A1: x". v1 in omega ;
thus A2: decode . (x". v1) = x. (card (x". v1)) by Def2
.= x. (x". v1) by CARD_1:def 5
.= v1 by Def3 ; :: thesis: ( (decode " ) . v1 = x". v1 & (f * decode ) . (x". v1) = f . v1 )
hence (decode " ) . v1 = x". v1 by Lm1, FUNCT_1:56; :: thesis: (f * decode ) . (x". v1) = f . v1
x". v1 in dom (f * decode ) by A1, Lm3;
hence (f * decode ) . (x". v1) = f . v1 by A2, FUNCT_1:22; :: thesis: verum