let S1, T1, S2, T2 be non empty RelStr ; :: thesis: ( RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of S2, the InternalRel of S2 #) & RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) implies for f1 being Function of S1,T1
for f2 being Function of S2,T2 st f1 = f2 holds
( ( f1 is infs-preserving implies f2 is infs-preserving ) & ( f1 is directed-sups-preserving implies f2 is directed-sups-preserving ) ) )
assume that
A1: RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of S2, the InternalRel of S2 #) and
A2: RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) ; :: thesis: for f1 being Function of S1,T1
for f2 being Function of S2,T2 st f1 = f2 holds
( ( f1 is infs-preserving implies f2 is infs-preserving ) & ( f1 is directed-sups-preserving implies f2 is directed-sups-preserving ) )
let f1 be Function of S1,T1; :: thesis: for f2 being Function of S2,T2 st f1 = f2 holds
( ( f1 is infs-preserving implies f2 is infs-preserving ) & ( f1 is directed-sups-preserving implies f2 is directed-sups-preserving ) )
let f2 be Function of S2,T2; :: thesis: ( f1 = f2 implies ( ( f1 is infs-preserving implies f2 is infs-preserving ) & ( f1 is directed-sups-preserving implies f2 is directed-sups-preserving ) ) )
assume A3: f1 = f2 ; :: thesis: ( ( f1 is infs-preserving implies f2 is infs-preserving ) & ( f1 is directed-sups-preserving implies f2 is directed-sups-preserving ) )
thus ( f1 is infs-preserving implies f2 is infs-preserving ) by A1, A2, A3, WAYBEL_0:65; :: thesis: ( f1 is directed-sups-preserving implies f2 is directed-sups-preserving )
assume A4: for X being Subset of S1 st not X is empty & X is directed holds
f1 preserves_sup_of X ; :: according to WAYBEL_0:def 37 :: thesis: f2 is directed-sups-preserving
let X be Subset of S2; :: according to WAYBEL_0:def 37 :: thesis: ( X is empty or not X is directed or f2 preserves_sup_of X )
reconsider Y = X as Subset of S1 by A1;
assume ( not X is empty & X is directed ) ; :: thesis: f2 preserves_sup_of X
then f1 preserves_sup_of Y by A1, A4, WAYBEL_0:3;
hence f2 preserves_sup_of X by A1, A2, A3, WAYBEL_0:65; :: thesis: verum