let f, g be Relation; :: thesis: for A, B being set st f | A = g | A & f | B = g | B holds
f | (A \/ B) = g | (A \/ B)
let A, B be set ; :: thesis: ( f | A = g | A & f | B = g | B implies f | (A \/ B) = g | (A \/ B) )
assume ( f | A = g | A & f | B = g | B ) ; :: thesis: f | (A \/ B) = g | (A \/ B)
hence f | (A \/ B) = (g | A) \/ (g | B) by Th72
.= g | (A \/ B) by Th72 ;
:: thesis: verum