let R, S, T be Relation; :: thesis: ( R,S are_isomorphic & S,T are_isomorphic implies R,T are_isomorphic )
given F being Function such that A1: F is_isomorphism_of R,S ; :: according to WELLORD1:def 8 :: thesis: ( not S,T are_isomorphic or R,T are_isomorphic )
given G being Function such that A2: G is_isomorphism_of S,T ; :: according to WELLORD1:def 8 :: thesis: R,T are_isomorphic
take G * F ; :: according to WELLORD1:def 8 :: thesis: G * F is_isomorphism_of R,T
thus G * F is_isomorphism_of R,T by A1, A2, Th41; :: thesis: verum