set O = OwnSymbolsOf S;
set f = I | (OwnSymbolsOf S);
set D = dom (I | (OwnSymbolsOf S));
set C = U \/ BOOLEAN;
( OwnSymbolsOf S c= dom (I | (OwnSymbolsOf S)) & dom (I | (OwnSymbolsOf S)) c= OwnSymbolsOf S ) by Lm2;
hence for b₁ being OwnSymbolsOf S -defined Relation st b₁ = I | (OwnSymbolsOf S) holds
b₁ is total by PARTFUN1:def 2, XBOOLE_0:def 10; :: thesis: verum