let L1, L2 be RelStr ; :: thesis: for f being Function of L1,L2 st f is isomorphic holds
( ( the carrier of L1 <> {} implies the carrier of L2 <> {} ) & ( the carrier of L2 <> {} implies the carrier of L1 <> {} ) & ( the carrier of L2 <> {} or the carrier of L1 = {} ) & ( the carrier of L1 = {} implies the carrier of L2 = {} ) & ( the carrier of L2 = {} implies the carrier of L1 = {} ) )
let f be Function of L1,L2; :: thesis: ( f is isomorphic implies ( ( the carrier of L1 <> {} implies the carrier of L2 <> {} ) & ( the carrier of L2 <> {} implies the carrier of L1 <> {} ) & ( the carrier of L2 <> {} or the carrier of L1 = {} ) & ( the carrier of L1 = {} implies the carrier of L2 = {} ) & ( the carrier of L2 = {} implies the carrier of L1 = {} ) ) )
assume A1: f is isomorphic ; :: thesis: ( ( the carrier of L1 <> {} implies the carrier of L2 <> {} ) & ( the carrier of L2 <> {} implies the carrier of L1 <> {} ) & ( the carrier of L2 <> {} or the carrier of L1 = {} ) & ( the carrier of L1 = {} implies the carrier of L2 = {} ) & ( the carrier of L2 = {} implies the carrier of L1 = {} ) )
( the carrier of L1 = {} iff the carrier of L2 = {} )
proof
hereby :: thesis: ( the carrier of L2 = {} implies the carrier of L1 = {} )
assume the carrier of L1 = {} ; :: thesis: the carrier of L2 = {}
then L1 is empty ;
then L2 is empty by A1, WAYBEL_0:def 38;
hence the carrier of L2 = {} ; :: thesis: verum
end;
assume the carrier of L2 = {} ; :: thesis: the carrier of L1 = {}
then L2 is empty ;
then L1 is empty by A1, WAYBEL_0:def 38;
hence the carrier of L1 = {} ; :: thesis: verum
end;
hence ( ( the carrier of L1 <> {} implies the carrier of L2 <> {} ) & ( the carrier of L2 <> {} implies the carrier of L1 <> {} ) & ( the carrier of L2 <> {} or the carrier of L1 = {} ) & ( the carrier of L1 = {} implies the carrier of L2 = {} ) & ( the carrier of L2 = {} implies the carrier of L1 = {} ) ) ; :: thesis: verum