let S be non empty finite set ; 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 * ; 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; Coim (((f 'or' g) * s),TRUE) = (Coim ((f * s),TRUE)) \/ (Coim ((g * s),TRUE))
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
; verum