let X, Y, Z be non empty set ; for R being RMembership_Func of X,Y
for S being RMembership_Func of Y,Z
for x being Element of X
for z being Element of Z holds
( rng (min (R,S,x,z)) = { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } & rng (min (R,S,x,z)) <> {} )
let R be RMembership_Func of X,Y; for S being RMembership_Func of Y,Z
for x being Element of X
for z being Element of Z holds
( rng (min (R,S,x,z)) = { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } & rng (min (R,S,x,z)) <> {} )
let S be RMembership_Func of Y,Z; for x being Element of X
for z being Element of Z holds
( rng (min (R,S,x,z)) = { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } & rng (min (R,S,x,z)) <> {} )
let x be Element of X; for z being Element of Z holds
( rng (min (R,S,x,z)) = { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } & rng (min (R,S,x,z)) <> {} )
let z be Element of Z; ( rng (min (R,S,x,z)) = { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } & rng (min (R,S,x,z)) <> {} )
set L = { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } ;
A1:
( Y = dom (min (R,S,x,z)) & min (R,S,x,z) is PartFunc of (dom (min (R,S,x,z))),(rng (min (R,S,x,z))) )
by FUNCT_2:def 1, RELSET_1:4;
for c being object holds
( c in { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } iff c in rng (min (R,S,x,z)) )
proof
let c be
object ;
( c in { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } iff c in rng (min (R,S,x,z)) )
hereby ( c in rng (min (R,S,x,z)) implies c in { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } )
assume
c in { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum }
;
c in rng (min (R,S,x,z))then consider y being
Element of
Y such that A2:
c = (R . [x,y]) "/\" (S . [y,z])
;
c = (min (R,S,x,z)) . y
by A2, FUZZY_4:def 2;
hence
c in rng (min (R,S,x,z))
by A1, PARTFUN1:4;
verum
end;
assume
c in rng (min (R,S,x,z))
;
c in { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum }
then consider y being
Element of
Y such that
y in dom (min (R,S,x,z))
and A3:
c = (min (R,S,x,z)) . y
by PARTFUN1:3;
c = (R . [x,y]) "/\" (S . [y,z])
by A3, FUZZY_4:def 2;
hence
c in { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum }
;
verum
end;
hence
rng (min (R,S,x,z)) = { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum }
by TARSKI:2; rng (min (R,S,x,z)) <> {}
thus
rng (min (R,S,x,z)) <> {}
; verum