let X, Y, Z be non empty set ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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)) )

ex d being set st d in rng (min (R,S,x,z))

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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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

hence
rng (min (R,S,x,z)) = { ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum }
by TARSKI:2; :: thesis: rng (min (R,S,x,z)) <> {}
let c be object ; :: thesis: ( c in { ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum } iff c in rng (min (R,S,x,z)) )

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 } ; :: thesis: verum

end;hereby :: thesis: ( 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 rng (min (R,S,x,z))
; :: thesis: 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 }
; :: thesis: 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; :: thesis: verum

end;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; :: thesis: 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 } ; :: thesis: verum

ex d being set st d in rng (min (R,S,x,z))

proof

hence
rng (min (R,S,x,z)) <> {}
; :: thesis: verum
set y = the Element of Y;

take (min (R,S,x,z)) . the Element of Y ; :: thesis: (min (R,S,x,z)) . the Element of Y in rng (min (R,S,x,z))

thus (min (R,S,x,z)) . the Element of Y in rng (min (R,S,x,z)) by A1, PARTFUN1:4; :: thesis: verum

end;take (min (R,S,x,z)) . the Element of Y ; :: thesis: (min (R,S,x,z)) . the Element of Y in rng (min (R,S,x,z))

thus (min (R,S,x,z)) . the Element of Y in rng (min (R,S,x,z)) by A1, PARTFUN1:4; :: thesis: verum