let S be non empty finite set ; :: thesis: for A, B being set
for f, g being Function of S,BOOLEAN st A c= S & B c= S & f = chi (A,S) & g = chi (B,S) holds
chi ((A \/ B),S) = f 'or' g
let A, B be set ; :: thesis: for f, g being Function of S,BOOLEAN st A c= S & B c= S & f = chi (A,S) & g = chi (B,S) holds
chi ((A \/ B),S) = f 'or' g
let f, g be Function of S,BOOLEAN; :: thesis: ( A c= S & B c= S & f = chi (A,S) & g = chi (B,S) implies chi ((A \/ B),S) = f 'or' g )
assume A1: ( A c= S & B c= S & f = chi (A,S) & g = chi (B,S) ) ; :: thesis: chi ((A \/ B),S) = f 'or' g
A2: dom (chi ((A \/ B),S)) = S by FUNCT_3:def 3;
A3: dom (chi (A,S)) = S by FUNCT_3:def 3;
A4: dom (chi (B,S)) = S by FUNCT_3:def 3;
A5: dom (f 'or' g) = (dom f) /\ (dom g) by BVFUNC_1:def 2
.= S by A1, A3, A4 ;
now :: thesis: for x being object st x in dom (f 'or' g) holds
(chi ((A \/ B),S)) . x = (f 'or' g) . x
let x be object ; :: thesis: ( x in dom (f 'or' g) implies (chi ((A \/ B),S)) . b1 = (f 'or' g) . b1 )
assume A6: x in dom (f 'or' g) ; :: thesis: (chi ((A \/ B),S)) . b1 = (f 'or' g) . b1
A7: x in (dom f) /\ (dom g) by A6, BVFUNC_1:def 2;
per cases ( (f 'or' g) . x = TRUE or (f 'or' g) . x <> TRUE ) ;
suppose A8: (f 'or' g) . x = TRUE ; :: thesis: (chi ((A \/ B),S)) . b1 = (f 'or' g) . b1
then ( (chi (A,S)) . x = 1 or (chi (B,S)) . x = 1 ) by A1, Lm2, A7;
then ( x in A or x in B ) by FUNCT_3:36;
then x in A \/ B by XBOOLE_0:def 3;
hence (chi ((A \/ B),S)) . x = (f 'or' g) . x by A8, A6, FUNCT_3:def 3; :: thesis: verum
end;
suppose A9: (f 'or' g) . x <> TRUE ; :: thesis: (chi ((A \/ B),S)) . b1 = (f 'or' g) . b1
A10: (f 'or' g) . x = FALSE by A9, XBOOLEAN:def 3;
( not (chi (A,S)) . x = 1 & not (chi (B,S)) . x = 1 ) by A1, A9, Lm2, A7;
then ( not x in A & not x in B ) by A6, FUNCT_3:def 3;
then not x in A \/ B by XBOOLE_0:def 3;
hence (chi ((A \/ B),S)) . x = (f 'or' g) . x by A10, A6, FUNCT_3:def 3; :: thesis: verum
end;
end;
end;
hence chi ((A \/ B),S) = f 'or' g by A2, A5, FUNCT_1:2; :: thesis: verum