let S be non empty finite set ; :: thesis: for s being Element of S *
for f, g being Function of S,BOOLEAN holds Coim (((f 'or' g) * s),TRUE) = (Coim ((f * s),TRUE)) \/ (Coim ((g * s),TRUE))
let s be Element of S * ; :: thesis: for f, g being Function of S,BOOLEAN holds Coim (((f 'or' g) * s),TRUE) = (Coim ((f * s),TRUE)) \/ (Coim ((g * s),TRUE))
let f, g be Function of S,BOOLEAN; :: thesis: Coim (((f 'or' g) * s),TRUE) = (Coim ((f * s),TRUE)) \/ (Coim ((g * s),TRUE))
A1: now :: thesis: for x being object holds
( x in (f 'or' g) " {TRUE} iff x in (f " {TRUE}) \/ (g " {TRUE}) )
let x be object ; :: thesis: ( x in (f 'or' g) " {TRUE} iff x in (f " {TRUE}) \/ (g " {TRUE}) )
A2: ( dom f = S & dom g = S ) by FUNCT_2:def 1;
A3: ( x in dom (f 'or' g) iff x in (dom f) /\ (dom g) ) by BVFUNC_1:def 2;
A4: ( x in (f 'or' g) " {TRUE} iff ( x in dom (f 'or' g) & (f 'or' g) . x in {TRUE} ) ) by FUNCT_1:def 7;
( x in dom (f 'or' g) & (f 'or' g) . x = TRUE iff ( x in (dom f) /\ (dom g) & ( f . x = TRUE or g . x = TRUE ) ) ) by Lm2, A3;
then ( x in (f 'or' g) " {TRUE} iff ( ( x in dom f & f . x in {TRUE} ) or ( x in dom g & g . x = TRUE ) ) ) by A4, A2, TARSKI:def 1;
then ( x in (f 'or' g) " {TRUE} iff ( x in f " {TRUE} or ( x in dom g & g . x in {TRUE} ) ) ) by FUNCT_1:def 7, TARSKI:def 1;
then ( x in (f 'or' g) " {TRUE} iff ( x in f " {TRUE} or x in g " {TRUE} ) ) by FUNCT_1:def 7;
hence ( x in (f 'or' g) " {TRUE} iff x in (f " {TRUE}) \/ (g " {TRUE}) ) by XBOOLE_0:def 3; :: thesis: verum
end;
thus Coim (((f 'or' g) * s),TRUE) = s " ((f 'or' g) " {TRUE}) by RELAT_1:146
.= s " ((f " {TRUE}) \/ (g " {TRUE})) by A1, TARSKI:2
.= (s " (f " {TRUE})) \/ (s " (g " {TRUE})) by RELAT_1:140
.= ((f * s) " {TRUE}) \/ (s " (g " {TRUE})) by RELAT_1:146
.= (Coim ((f * s),TRUE)) \/ (Coim ((g * s),TRUE)) by RELAT_1:146 ; :: thesis: verum