let f be Function of LTLB_WFF,BOOLEAN; :: thesis: for p, q being Element of LTLB_WFF holds (VAL f) . (p '&&' q) = ((VAL f) . p) '&' ((VAL f) . q)
let p, q be Element of LTLB_WFF ; :: thesis: (VAL f) . (p '&&' q) = ((VAL f) . p) '&' ((VAL f) . q)
A1: ( (VAL f) . p = 0 or (VAL f) . p = 1 ) by XBOOLEAN:def 3;
A2: ( (VAL f) . q = 0 or (VAL f) . q = 1 ) by XBOOLEAN:def 3;
thus (VAL f) . (p '&&' q) = ((VAL f) . (p => (q => TFALSUM))) => ((VAL f) . TFALSUM) by Def15
.= (((VAL f) . p) => ((VAL f) . (q => TFALSUM))) => ((VAL f) . TFALSUM) by Def15
.= (((VAL f) . p) => (((VAL f) . q) => ((VAL f) . TFALSUM))) => ((VAL f) . TFALSUM) by Def15
.= (((VAL f) /. p) => (((VAL f) . q) => FALSE)) => ((VAL f) . TFALSUM) by Def15
.= ((VAL f) . p) '&' ((VAL f) . q) by A1, A2, Def15 ; :: thesis: verum